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

Theorem nfeld 2991
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 2897 . 2 (𝐴𝐵 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝐵))
2 nfv 1916 . . 3 𝑦𝜑
3 nfcvd 2981 . . . . 5 (𝜑𝑥𝑦)
4 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
53, 4nfeqd 2990 . . . 4 (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
76nfcrd 2970 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
85, 7nfand 1899 . . 3 (𝜑 → Ⅎ𝑥(𝑦 = 𝐴𝑦𝐵))
92, 8nfexd 2350 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦 = 𝐴𝑦𝐵))
101, 9nfxfrd 1855 1 (𝜑 → Ⅎ𝑥 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wex 1781  wnf 1785  wcel 2115  wnfc 2962
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-cleq 2817  df-clel 2896  df-nfc 2964
This theorem is referenced by:  nfel  2994  nfneld  3125  nfraldw  3217  nfrald  3218  ralcom2  3354  nfreud  3363  nfrmod  3364  nfreuw  3365  nfrmow  3366  nfrmo  3368  nfsbc1d  3775  nfsbcdw  3778  nfsbcd  3781  sbcrext  3839  nfdisjw  5024  nfdisj  5025  nfbrd  5093  nfriotadw  7104  nfriotad  7107  nfixpw  8463  nfixp  8464  axrepndlem2  10000  axrepnd  10001  axunnd  10003  axpowndlem2  10005  axpowndlem3  10006  axpowndlem4  10007  axpownd  10008  axregndlem2  10010  axinfndlem1  10012  axinfnd  10013  axacndlem4  10017  axacndlem5  10018  axacnd  10019
  Copyright terms: Public domain W3C validator