New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfeq Unicode version

Theorem nfeq 2496
 Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfnfc.1
nfeq.2
Assertion
Ref Expression
nfeq

Proof of Theorem nfeq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2347 . 2
2 nfnfc.1 . . . . 5
32nfcri 2483 . . . 4
4 nfeq.2 . . . . 5
54nfcri 2483 . . . 4
63, 5nfbi 1834 . . 3
76nfal 1842 . 2
81, 7nfxfr 1570 1
 Colors of variables: wff setvar class Syntax hints:   wb 176  wal 1540  wnf 1544   wceq 1642   wcel 1710  wnfc 2476 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-cleq 2346  df-clel 2349  df-nfc 2478 This theorem is referenced by:  nfel  2497  nfeq1  2498  nfeq2  2500  nfne  2610  raleqf  2803  rexeqf  2804  reueq1f  2805  rmoeq1f  2806  rabeqf  2852  sbceqg  3152  csbhypf  3171  nffn  5180  nffo  5268  eqfnfv2f  5396  dff13f  5472  ov2gf  5711  fvmptf  5722
 Copyright terms: Public domain W3C validator