ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfeq GIF version

Theorem nfeq 2236
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 2082 . 2 (𝐴 = 𝐵 ↔ ∀𝑧(𝑧𝐴𝑧𝐵))
2 nfnfc.1 . . . . 5 𝑥𝐴
32nfcri 2222 . . . 4 𝑥 𝑧𝐴
4 nfeq.2 . . . . 5 𝑥𝐵
54nfcri 2222 . . . 4 𝑥 𝑧𝐵
63, 5nfbi 1526 . . 3 𝑥(𝑧𝐴𝑧𝐵)
76nfal 1513 . 2 𝑥𝑧(𝑧𝐴𝑧𝐵)
81, 7nfxfr 1408 1 𝑥 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:  wb 103  wal 1287   = wceq 1289  wnf 1394  wcel 1438  wnfc 2215
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-tru 1292  df-nf 1395  df-sb 1693  df-cleq 2081  df-clel 2084  df-nfc 2217
This theorem is referenced by:  nfel  2237  nfeq1  2238  nfeq2  2240  nfne  2348  raleqf  2558  rexeqf  2559  reueq1f  2560  rmoeq1f  2561  rabeqf  2609  sbceqg  2945  csbhypf  2964  nfiotadxy  4970  nffn  5096  nffo  5216  fvmptdf  5374  mpteqb  5377  fvmptf  5379  eqfnfv2f  5385  dff13f  5531  ovmpt2s  5750  ov2gf  5751  ovmpt2dxf  5752  ovmpt2df  5758  eqerlem  6303  sumeq2  10712  fsumadd  10763
  Copyright terms: Public domain W3C validator