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

Theorem nfel 2440
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 2292 . 2  |-  ( A  e.  B  <->  E. z
( z  =  A  /\  z  e.  B
) )
2 nfcv 2432 . . . . 5  |-  F/_ x
z
3 nfnfc.1 . . . . 5  |-  F/_ x A
42, 3nfeq 2439 . . . 4  |-  F/ x  z  =  A
5 nfeq.2 . . . . 5  |-  F/_ x B
65nfcri 2426 . . . 4  |-  F/ x  z  e.  B
74, 6nfan 1783 . . 3  |-  F/ x
( z  =  A  /\  z  e.  B
)
87nfex 1779 . 2  |-  F/ x E. z ( z  =  A  /\  z  e.  B )
91, 8nfxfr 1560 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1531   F/wnf 1534    = wceq 1632    e. wcel 1696   F/_wnfc 2419
This theorem is referenced by:  nfel1  2442  nfel2  2444  nfnel  2553  elabgf  2925  elrabf  2935  sbcel12g  3109  rabxfrd  4571  ffnfvf  5702  mptelixpg  6869  ac6num  8122  dprd2d2  15295  ptcldmpt  17324  prdsdsf  17947  prdsxmet  17949  abrexss  23056  clelsb3f  23158  ssiun2sf  23173  rmo3f  23194  rmo4fOLD  23195  suppss2f  23216  cbvmptf  23235  fmptcof2  23244  funcnv4mpt  23252  cbvdisjf  23365  disjabrexf  23375  iundisjfi  23378  esumcl  23428  esum0  23443  esumcst  23451  itgabsnc  25020  aomclem8  27262  flcidc  27482  elunif  27790  rspcegf  27797  refsumcn  27804  rfcnnnub  27810  fmul01  27813  fmuldfeqlem1  27815  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climmulf  27833  climsuse  27837  climrecf  27838  stoweidlem3  27855  stoweidlem16  27868  stoweidlem19  27871  stoweidlem22  27874  stoweidlem26  27878  stoweidlem27  27879  stoweidlem28  27880  stoweidlem29  27881  stoweidlem31  27883  stoweidlem34  27886  stoweidlem35  27887  stoweidlem36  27888  stoweidlem42  27894  stoweidlem46  27898  stoweidlem48  27900  stoweidlem51  27903  stoweidlem57  27909  stoweidlem59  27911  stirlinglem5  27930  eu2ndop1stv  28083  nfdfat  28098  bnj1491  29403
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421
  Copyright terms: Public domain W3C validator