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

Theorem nfeld 2587
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 2432 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1629 . . 3  |-  F/ y
ph
3 nfcvd 2573 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2586 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2585 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 1843 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 1873 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1580 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1550   F/wnf 1553    = wceq 1652    e. wcel 1725   F/_wnfc 2559
This theorem is referenced by:  nfneld  2703  nfrald  2757  ralcom2  2872  nfreud  2880  nfrmod  2881  nfrmo  2883  nfsbc1d  3178  nfsbcd  3181  sbcrext  3234  nfdisj  4194  nfbrd  4255  nfriotad  6558  riotasvdOLD  6593  riotasv2dOLD  6595  riotasv3dOLD  6599  nfixp  7081  axrepndlem2  8468  axrepnd  8469  axunnd  8471  axpowndlem2  8473  axpowndlem3  8474  axpowndlem4  8475  axpownd  8476  axregndlem2  8478  axinfndlem1  8480  axinfnd  8481  axacndlem4  8485  axacndlem5  8486  axacnd  8487
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-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-cleq 2429  df-clel 2432  df-nfc 2561
  Copyright terms: Public domain W3C validator