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

Theorem nfeld 2434
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 2279 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1605 . . 3  |-  F/ y
ph
3 nfcvd 2420 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2433 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2432 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 1763 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 1776 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1558 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   E.wex 1528   F/wnf 1531    = wceq 1623    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  nfneld  2542  nfrald  2594  ralcom2  2704  nfreud  2712  nfrmod  2713  nfrmo  2715  nfsbc1d  3008  nfsbcd  3011  sbcrext  3064  nfdisj  4005  nfbrd  4066  nfriotad  6313  riotasvdOLD  6348  riotasv2dOLD  6350  riotasv3dOLD  6354  nfixp  6835  axextnd  8213  axrepndlem2  8215  axrepnd  8216  axunndlem1  8217  axunnd  8218  axpowndlem2  8220  axpowndlem3  8221  axpowndlem4  8222  axpownd  8223  axregndlem2  8225  axregnd  8226  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234  axextdist  24156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator