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

Theorem nfeld 2759
 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 2606 . 2 (𝐴𝐵 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝐵))
2 nfv 1830 . . 3 𝑦𝜑
3 nfcvd 2752 . . . . 5 (𝜑𝑥𝑦)
4 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
53, 4nfeqd 2758 . . . 4 (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
76nfcrd 2757 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
85, 7nfand 1814 . . 3 (𝜑 → Ⅎ𝑥(𝑦 = 𝐴𝑦𝐵))
92, 8nfexd 2153 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦 = 𝐴𝑦𝐵))
101, 9nfxfrd 1772 1 (𝜑 → Ⅎ𝑥 𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475  ∃wex 1695  Ⅎwnf 1699   ∈ wcel 1977  Ⅎwnfc 2738 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701  df-cleq 2603  df-clel 2606  df-nfc 2740 This theorem is referenced by:  nfel  2763  nfneld  2891  nfrald  2928  ralcom2  3083  nfreud  3091  nfrmod  3092  nfrmo  3094  nfsbc1d  3420  nfsbcd  3423  sbcrext  3478  sbcrextOLD  3479  nfdisj  4565  nfbrd  4628  nfriotad  6519  nfixp  7813  axrepndlem2  9294  axrepnd  9295  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axpownd  9302  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  nfintd  42218
 Copyright terms: Public domain W3C validator