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

Theorem nfeld 2624
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 2449 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1712 . . 3  |-  F/ y
ph
3 nfcvd 2617 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2623 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2622 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 1930 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 1957 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1651 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398   E.wex 1617   F/wnf 1621    e. wcel 1823   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-cleq 2446  df-clel 2449  df-nfc 2604
This theorem is referenced by:  nfel  2629  nfneld  2798  nfrald  2839  ralcom2  3019  nfreud  3027  nfrmod  3028  nfrmo  3030  nfsbc1d  3342  nfsbcd  3345  sbcrext  3398  nfdisj  4422  nfbrd  4482  nfriotad  6240  nfixp  7481  axrepndlem2  8959  axrepnd  8960  axunnd  8962  axpowndlem2  8964  axpowndlem3  8965  axpowndlem4  8966  axpownd  8967  axregndlem2  8969  axinfndlem1  8972  axinfnd  8973  axacndlem4  8977  axacndlem5  8978  axacnd  8979
  Copyright terms: Public domain W3C validator