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

Theorem nfeld 2627
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 2452 . 2
2 nfv 1707 . . 3
3 nfcvd 2620 . . . . 5
4 nfeqd.1 . . . . 5
53, 4nfeqd 2626 . . . 4
6 nfeqd.2 . . . . 5
76nfcrd 2625 . . . 4
85, 7nfand 1925 . . 3
92, 8nfexd 1952 . 2
101, 9nfxfrd 1646 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  E.wex 1612  F/wnf 1616  e.wcel 1818  F/_wnfc 2605
This theorem is referenced by:  nfel  2632  nfneld  2801  nfrald  2842  ralcom2  3022  nfreud  3030  nfrmod  3031  nfrmo  3033  nfsbc1d  3345  nfsbcd  3348  sbcrextOLD  3409  sbcrext  3410  nfdisj  4434  nfbrd  4495  nfriotad  6265  nfixp  7508  axrepndlem2  8989  axrepnd  8990  axunnd  8992  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axpownd  8999  axregndlem2  9001  axinfndlem1  9004  axinfnd  9005  axacndlem4  9009  axacndlem5  9010  axacnd  9011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607
  Copyright terms: Public domain W3C validator