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

Theorem nfelOLD 2605
 Description: Obsolete proof of nfel 2604 as of 16-Nov-2019. (Contributed by NM, 1-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
nfnfc.1
nfeq.2
Assertion
Ref Expression
nfelOLD

Proof of Theorem nfelOLD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-clel 2424 . 2
2 nfcv 2591 . . . . 5
3 nfnfc.1 . . . . 5
42, 3nfeq 2602 . . . 4
5 nfeq.2 . . . . 5
65nfcri 2584 . . . 4
74, 6nfan 1986 . . 3
87nfex 2006 . 2
91, 8nfxfr 1692 1
 Colors of variables: wff setvar class Syntax hints:   wa 370   wceq 1437  wex 1659  wnf 1663   wcel 1870  wnfc 2577 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-cleq 2421  df-clel 2424  df-nfc 2579 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator