MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfel Unicode version

Theorem nfel 2427
Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfnfc.1  |-  F/_ x A
nfeq.2  |-  F/_ x B
Assertion
Ref Expression
nfel  |-  F/ x  A  e.  B

Proof of Theorem nfel
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 df-clel 2279 . 2  |-  ( A  e.  B  <->  E. z
( z  =  A  /\  z  e.  B
) )
2 nfcv 2419 . . . . 5  |-  F/_ x
z
3 nfnfc.1 . . . . 5  |-  F/_ x A
42, 3nfeq 2426 . . . 4  |-  F/ x  z  =  A
5 nfeq.2 . . . . 5  |-  F/_ x B
65nfcri 2413 . . . 4  |-  F/ x  z  e.  B
74, 6nfan 1771 . . 3  |-  F/ x
( z  =  A  /\  z  e.  B
)
87nfex 1767 . 2  |-  F/ x E. z ( z  =  A  /\  z  e.  B )
91, 8nfxfr 1557 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1528   F/wnf 1531    = wceq 1623    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  nfel1  2429  nfel2  2431  nfnel  2540  elabgf  2912  elrabf  2922  sbcel12g  3096  rabxfrd  4555  ffnfvf  5686  mptelixpg  6853  ac6num  8106  dprd2d2  15279  ptcldmpt  17308  prdsdsf  17931  prdsxmet  17933  abrexss  23040  clelsb3f  23142  ssiun2sf  23157  rmo3f  23178  rmo4fOLD  23179  suppss2f  23201  cbvmptf  23220  fmptcof2  23229  funcnv4mpt  23237  cbvdisjf  23350  disjabrexf  23360  iundisjfi  23363  esumcl  23413  esum0  23428  esumcst  23436  aomclem8  27159  flcidc  27379  elunif  27687  rspcegf  27694  refsumcn  27701  rfcnnnub  27707  fmul01  27710  fmuldfeqlem1  27712  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climmulf  27730  climsuse  27734  climrecf  27735  stoweidlem3  27752  stoweidlem16  27765  stoweidlem19  27768  stoweidlem22  27771  stoweidlem26  27775  stoweidlem27  27776  stoweidlem28  27777  stoweidlem29  27778  stoweidlem31  27780  stoweidlem34  27783  stoweidlem35  27784  stoweidlem36  27785  stoweidlem42  27791  stoweidlem46  27795  stoweidlem48  27797  stoweidlem51  27800  stoweidlem57  27806  stoweidlem59  27808  stirlinglem5  27827  nfdfat  27993  bnj1491  29087
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator