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

Theorem nfeld 2447
Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfeqd.1  |-  ( ph  -> 
F/_ x A )
nfeqd.2  |-  ( ph  -> 
F/_ x B )
Assertion
Ref Expression
nfeld  |-  ( ph  ->  F/ x  A  e.  B )

Proof of Theorem nfeld
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-clel 2292 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1609 . . 3  |-  F/ y
ph
3 nfcvd 2433 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2446 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2445 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 1775 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 1788 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1561 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1531   F/wnf 1534    = wceq 1632    e. wcel 1696   F/_wnfc 2419
This theorem is referenced by:  nfneld  2555  nfrald  2607  ralcom2  2717  nfreud  2725  nfrmod  2726  nfrmo  2728  nfsbc1d  3021  nfsbcd  3024  sbcrext  3077  nfdisj  4021  nfbrd  4082  nfriotad  6329  riotasvdOLD  6364  riotasv2dOLD  6366  riotasv3dOLD  6370  nfixp  6851  axextnd  8229  axrepndlem2  8231  axrepnd  8232  axunndlem1  8233  axunnd  8234  axpowndlem2  8236  axpowndlem3  8237  axpowndlem4  8238  axpownd  8239  axregndlem2  8241  axregnd  8242  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  axextdist  24227
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-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-cleq 2289  df-clel 2292  df-nfc 2421
  Copyright terms: Public domain W3C validator