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

Theorem nfeld 2916
Description: Hypothesis builder for elementhood. (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfeqd.1 (𝜑𝑥𝐴)
nfeqd.2 (𝜑𝑥𝐵)
Assertion
Ref Expression
nfeld (𝜑 → Ⅎ𝑥 𝐴𝐵)

Proof of Theorem nfeld
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 dfclel 2815 . 2 (𝐴𝐵 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝐵))
2 nfv 1917 . . 3 𝑦𝜑
3 nfcvd 2906 . . . . 5 (𝜑𝑥𝑦)
4 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
53, 4nfeqd 2915 . . . 4 (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
76nfcrd 2894 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
85, 7nfand 1900 . . 3 (𝜑 → Ⅎ𝑥(𝑦 = 𝐴𝑦𝐵))
92, 8nfexd 2322 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦 = 𝐴𝑦𝐵))
101, 9nfxfrd 1856 1 (𝜑 → Ⅎ𝑥 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wex 1781  wnf 1785  wcel 2106  wnfc 2885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2814  df-nfc 2887
This theorem is referenced by:  nfel  2919  nfneld  3055  nfraldwOLD  3300  nfrald  3343  ralcom2  3348  nfreuwOLD  3395  nfrmowOLD  3396  nfrmod  3401  nfreud  3402  nfrmo  3403  nfsbc1d  3755  nfsbcdw  3758  nfsbcd  3761  sbcrext  3827  nfdisjw  5080  nfdisj  5081  nfbrd  5149  nfriotadw  7317  nfriotad  7321  nfixpw  8850  nfixp  8851  axrepndlem2  10525  axrepnd  10526  axunnd  10528  axpowndlem2  10530  axpowndlem3  10531  axpowndlem4  10532  axpownd  10533  axregndlem2  10535  axinfndlem1  10537  axinfnd  10538  axacndlem4  10542  axacndlem5  10543  axacnd  10544
  Copyright terms: Public domain W3C validator