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

Theorem nfeld 2943
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 df-clel 2774 . 2 (𝐴𝐵 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝐵))
2 nfv 1957 . . 3 𝑦𝜑
3 nfcvd 2935 . . . . 5 (𝜑𝑥𝑦)
4 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
53, 4nfeqd 2942 . . . 4 (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
76nfcrd 2927 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
85, 7nfand 1944 . . 3 (𝜑 → Ⅎ𝑥(𝑦 = 𝐴𝑦𝐵))
92, 8nfexd 2305 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦 = 𝐴𝑦𝐵))
101, 9nfxfrd 1898 1 (𝜑 → Ⅎ𝑥 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wex 1823  wnf 1827  wcel 2107  wnfc 2919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828  df-cleq 2770  df-clel 2774  df-nfc 2921
This theorem is referenced by:  nfel  2946  nfneld  3083  nfrald  3126  ralcom2  3290  nfreud  3298  nfrmod  3299  nfrmo  3301  nfsbc1d  3670  nfsbcd  3673  sbcrext  3729  nfdisj  4866  nfbrd  4932  nfriotad  6891  nfixp  8213  axrepndlem2  9750  axrepnd  9751  axunnd  9753  axpowndlem2  9755  axpowndlem3  9756  axpowndlem4  9757  axpownd  9758  axregndlem2  9760  axinfndlem1  9762  axinfnd  9763  axacndlem4  9767  axacndlem5  9768  axacnd  9769
  Copyright terms: Public domain W3C validator