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

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

Proof of Theorem nfeq
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2347 . 2 (A = Bz(z Az B))
2 nfnfc.1 . . . . 5 xA
32nfcri 2483 . . . 4 x z A
4 nfeq.2 . . . . 5 xB
54nfcri 2483 . . . 4 x z B
63, 5nfbi 1834 . . 3 x(z Az B)
76nfal 1842 . 2 xz(z Az B)
81, 7nfxfr 1570 1 x A = B
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