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

Theorem nfeld 2618
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 2445 . 2  |-  ( A  e.  B  <->  E. y
( y  =  A  /\  y  e.  B
) )
2 nfv 1674 . . 3  |-  F/ y
ph
3 nfcvd 2611 . . . . 5  |-  ( ph  -> 
F/_ x y )
4 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
53, 4nfeqd 2617 . . . 4  |-  ( ph  ->  F/ x  y  =  A )
6 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
76nfcrd 2616 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
85, 7nfand 1859 . . 3  |-  ( ph  ->  F/ x ( y  =  A  /\  y  e.  B ) )
92, 8nfexd 1879 . 2  |-  ( ph  ->  F/ x E. y
( y  =  A  /\  y  e.  B
) )
101, 9nfxfrd 1617 1  |-  ( ph  ->  F/ x  A  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370   E.wex 1587   F/wnf 1590    e. wcel 1757   F/_wnfc 2596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-cleq 2442  df-clel 2445  df-nfc 2598
This theorem is referenced by:  nfel  2622  nfneld  2789  nfrald  2853  ralcom2  2967  nfreud  2975  nfrmod  2976  nfrmo  2978  nfsbc1d  3288  nfsbcd  3291  sbcrextOLD  3352  sbcrext  3353  nfdisj  4358  nfbrd  4419  nfriotad  6145  nfixp  7368  axrepndlem2  8844  axrepnd  8845  axunnd  8847  axpowndlem2  8849  axpowndlem2OLD  8850  axpowndlem3  8851  axpowndlem3OLD  8852  axpowndlem4  8853  axpownd  8854  axregndlem2  8856  axinfndlem1  8859  axinfnd  8860  axacndlem4  8864  axacndlem5  8865  axacnd  8866
  Copyright terms: Public domain W3C validator