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

Theorem nfel 2582
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 2434 . 2  |-  ( A  e.  B  <->  E. z
( z  =  A  /\  z  e.  B
) )
2 nfcv 2574 . . . . 5  |-  F/_ x
z
3 nfnfc.1 . . . . 5  |-  F/_ x A
42, 3nfeq 2581 . . . 4  |-  F/ x  z  =  A
5 nfeq.2 . . . . 5  |-  F/_ x B
65nfcri 2568 . . . 4  |-  F/ x  z  e.  B
74, 6nfan 1860 . . 3  |-  F/ x
( z  =  A  /\  z  e.  B
)
87nfex 1873 . 2  |-  F/ x E. z ( z  =  A  /\  z  e.  B )
91, 8nfxfr 1615 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369   E.wex 1586   F/wnf 1589    e. wcel 1756   F/_wnfc 2561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2431  df-clel 2434  df-nfc 2563
This theorem is referenced by:  nfel1  2584  nfel2  2586  nfnel  2707  elabgf  3099  elrabf  3110  sbcel12  3670  sbcel12gOLD  3671  rabxfrd  4508  ffnfvf  5865  mptelixpg  7292  ac6num  8640  ptcldmpt  19162  prdsdsf  19917  prdsxmet  19919  rmo4fOLD  25831  ssiun2sf  25861  ssrelf  25896  funcnv4mpt  25940  nnindf  26040  oms0  26662  ptrest  28378  aomclem8  29367  elunif  29691  rspcegf  29698  climsuse  29734  stoweidlem59  29807  nfdfat  29989  ovmpt3rab1  30114  bnj1491  31935
  Copyright terms: Public domain W3C validator