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

Theorem nfeld 2903
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 2803 . 2 (𝐴𝐵 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝐵))
2 nfv 1909 . . 3 𝑦𝜑
3 nfcvd 2892 . . . . 5 (𝜑𝑥𝑦)
4 nfeqd.1 . . . . 5 (𝜑𝑥𝐴)
53, 4nfeqd 2902 . . . 4 (𝜑 → Ⅎ𝑥 𝑦 = 𝐴)
6 nfeqd.2 . . . . 5 (𝜑𝑥𝐵)
76nfcrd 2884 . . . 4 (𝜑 → Ⅎ𝑥 𝑦𝐵)
85, 7nfand 1892 . . 3 (𝜑 → Ⅎ𝑥(𝑦 = 𝐴𝑦𝐵))
92, 8nfexd 2317 . 2 (𝜑 → Ⅎ𝑥𝑦(𝑦 = 𝐴𝑦𝐵))
101, 9nfxfrd 1848 1 (𝜑 → Ⅎ𝑥 𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wex 1773  wnf 1777  wcel 2098  wnfc 2875
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778  df-cleq 2717  df-clel 2802  df-nfc 2877
This theorem is referenced by:  nfel  2906  nfneld  3044  nfraldwOLD  3308  nfrald  3355  ralcom2  3360  nfreuwOLD  3408  nfrmowOLD  3409  nfrmod  3414  nfreud  3415  nfrmo  3416  nfsbc1d  3791  nfsbcdw  3794  nfsbcd  3797  sbcrext  3863  nfdisjw  5126  nfdisj  5127  nfbrd  5195  nfriotadw  7383  nfriotad  7387  nfixpw  8935  nfixp  8936  axrepndlem2  10623  axrepnd  10624  axunnd  10626  axpowndlem2  10628  axpowndlem3  10629  axpowndlem4  10630  axpownd  10631  axregndlem2  10633  axinfndlem1  10635  axinfnd  10636  axacndlem4  10640  axacndlem5  10641  axacnd  10642
  Copyright terms: Public domain W3C validator