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

Theorem nfeld 2599
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 2424 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1754 . . 3  |-  F/ y
ph
3 nfcvd 2592 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2598 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2597 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 1983 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 2010 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1693 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437   E.wex 1659   F/wnf 1663    e. wcel 1870   F/_wnfc 2577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664  df-cleq 2421  df-clel 2424  df-nfc 2579
This theorem is referenced by:  nfel  2604  nfneld  2776  nfrald  2817  ralcom2  3000  nfreud  3008  nfrmod  3009  nfrmo  3011  nfsbc1d  3323  nfsbcd  3326  sbcrext  3379  nfdisj  4409  nfbrd  4469  nfriotad  6275  nfixp  7549  axrepndlem2  9016  axrepnd  9017  axunnd  9019  axpowndlem2  9021  axpowndlem3  9022  axpowndlem4  9023  axpownd  9024  axregndlem2  9026  axinfndlem1  9029  axinfnd  9030  axacndlem4  9034  axacndlem5  9035  axacnd  9036
  Copyright terms: Public domain W3C validator