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

Theorem nfeld 2770
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 2616 . 2 (𝐴𝐵 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝐵))
2 nfv 1841 . . 3 𝑦𝜑
3 nfcvd 2763 . . . . 5 (𝜑𝑥𝑦)
4 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
53, 4nfeqd 2769 . . . 4 (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
76nfcrd 2768 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
85, 7nfand 1824 . . 3 (𝜑 → Ⅎ𝑥(𝑦 = 𝐴𝑦𝐵))
92, 8nfexd 2165 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦 = 𝐴𝑦𝐵))
101, 9nfxfrd 1778 1 (𝜑 → Ⅎ𝑥 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  wex 1702  wnf 1706  wcel 1988  wnfc 2749
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1703  df-nf 1708  df-cleq 2613  df-clel 2616  df-nfc 2751
This theorem is referenced by:  nfel  2774  nfneld  2902  nfrald  2941  ralcom2  3099  nfreud  3107  nfrmod  3108  nfrmo  3110  nfsbc1d  3447  nfsbcd  3450  sbcrext  3505  sbcrextOLD  3506  nfdisj  4623  nfbrd  4689  nfriotad  6604  nfixp  7912  axrepndlem2  9400  axrepnd  9401  axunnd  9403  axpowndlem2  9405  axpowndlem3  9406  axpowndlem4  9407  axpownd  9408  axregndlem2  9410  axinfndlem1  9412  axinfnd  9413  axacndlem4  9417  axacndlem5  9418  axacnd  9419
  Copyright terms: Public domain W3C validator