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

Theorem nfel 2579
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 2431 . 2  |-  ( A  e.  B  <->  E. z
( z  =  A  /\  z  e.  B
) )
2 nfcv 2571 . . . . 5  |-  F/_ x
z
3 nfnfc.1 . . . . 5  |-  F/_ x A
42, 3nfeq 2578 . . . 4  |-  F/ x  z  =  A
5 nfeq.2 . . . . 5  |-  F/_ x B
65nfcri 2565 . . . 4  |-  F/ x  z  e.  B
74, 6nfan 1846 . . 3  |-  F/ x
( z  =  A  /\  z  e.  B
)
87nfex 1865 . 2  |-  F/ x E. z ( z  =  A  /\  z  e.  B )
91, 8nfxfr 1579 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1550   F/wnf 1553    = wceq 1652    e. wcel 1725   F/_wnfc 2558
This theorem is referenced by:  nfel1  2581  nfel2  2583  nfnel  2694  elabgf  3072  elrabf  3083  sbcel12g  3258  rabxfrd  4736  ffnfvf  5887  mptelixpg  7091  ac6num  8351  ptcldmpt  17638  prdsdsf  18389  prdsxmet  18391  rmo4fOLD  23975  ssiun2sf  24002  funcnv4mpt  24077  aomclem8  27117  elunif  27644  rspcegf  27651  climsuse  27691  stoweidlem59  27765  nfdfat  27951  bnj1491  29353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560
  Copyright terms: Public domain W3C validator