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

Theorem nfeld 2611
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 2458 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1772 . . 3  |-  F/ y
ph
3 nfcvd 2604 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2610 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2609 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 2019 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 2046 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1708 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    = wceq 1455   E.wex 1674   F/wnf 1678    e. wcel 1898   F/_wnfc 2590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679  df-cleq 2455  df-clel 2458  df-nfc 2592
This theorem is referenced by:  nfel  2615  nfneld  2744  nfrald  2785  ralcom2  2967  nfreud  2975  nfrmod  2976  nfrmo  2978  nfsbc1d  3297  nfsbcd  3300  sbcrext  3353  nfdisj  4399  nfbrd  4460  nfriotad  6285  nfixp  7567  axrepndlem2  9044  axrepnd  9045  axunnd  9047  axpowndlem2  9049  axpowndlem3  9050  axpowndlem4  9051  axpownd  9052  axregndlem2  9054  axinfndlem1  9056  axinfnd  9057  axacndlem4  9061  axacndlem5  9062  axacnd  9063
  Copyright terms: Public domain W3C validator