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

Theorem nfel 2531
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 2383 . 2  |-  ( A  e.  B  <->  E. z
( z  =  A  /\  z  e.  B
) )
2 nfcv 2523 . . . . 5  |-  F/_ x
z
3 nfnfc.1 . . . . 5  |-  F/_ x A
42, 3nfeq 2530 . . . 4  |-  F/ x  z  =  A
5 nfeq.2 . . . . 5  |-  F/_ x B
65nfcri 2517 . . . 4  |-  F/ x  z  e.  B
74, 6nfan 1836 . . 3  |-  F/ x
( z  =  A  /\  z  e.  B
)
87nfex 1855 . 2  |-  F/ x E. z ( z  =  A  /\  z  e.  B )
91, 8nfxfr 1576 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1547   F/wnf 1550    = wceq 1649    e. wcel 1717   F/_wnfc 2510
This theorem is referenced by:  nfel1  2533  nfel2  2535  nfnel  2646  elabgf  3023  elrabf  3034  sbcel12g  3209  rabxfrd  4684  ffnfvf  5834  mptelixpg  7035  ac6num  8292  ptcldmpt  17567  prdsdsf  18305  prdsxmet  18307  rmo4fOLD  23827  ssiun2sf  23854  funcnv4mpt  23926  aomclem8  26828  elunif  27355  rspcegf  27362  climsuse  27402  stoweidlem59  27476  nfdfat  27663  bnj1491  28764
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2380  df-clel 2383  df-nfc 2512
  Copyright terms: Public domain W3C validator