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

Theorem nfeld 2588
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 2417 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1755 . . 3  |-  F/ y
ph
3 nfcvd 2581 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2587 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2586 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 1985 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 2012 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1691 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   E.wex 1657   F/wnf 1661    e. wcel 1872   F/_wnfc 2566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-nf 1662  df-cleq 2414  df-clel 2417  df-nfc 2568
This theorem is referenced by:  nfel  2593  nfneld  2765  nfrald  2807  ralcom2  2990  nfreud  2998  nfrmod  2999  nfrmo  3001  nfsbc1d  3317  nfsbcd  3320  sbcrext  3373  nfdisj  4406  nfbrd  4467  nfriotad  6275  nfixp  7552  axrepndlem2  9025  axrepnd  9026  axunnd  9028  axpowndlem2  9030  axpowndlem3  9031  axpowndlem4  9032  axpownd  9033  axregndlem2  9035  axinfndlem1  9037  axinfnd  9038  axacndlem4  9042  axacndlem5  9043  axacnd  9044
  Copyright terms: Public domain W3C validator