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

Theorem nfeq 2167
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 2016 . 2 (A = Bz(z Az B))
2 nfnfc.1 . . . . 5 xA
32nfcri 2154 . . . 4 x z A
4 nfeq.2 . . . . 5 xB
54nfcri 2154 . . . 4 x z B
63, 5nfbi 1463 . . 3 x(z Az B)
76nfal 1450 . 2 xz(z Az B)
81, 7nfxfr 1343 1 x A = B
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1226   = wceq 1228  wnf 1329   wcel 1374  wnfc 2147
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1628  df-cleq 2015  df-clel 2018  df-nfc 2149
This theorem is referenced by:  nfel  2168  nfeq1  2169  nfeq2  2171  nfne  2273  raleqf  2477  rexeqf  2478  reueq1f  2479  rmoeq1f  2480  rabeqf  2526  sbceqg  2841  csbhypf  2860  nfiotadxy  4795  nffn  4919  nffo  5028  fvmptdf  5181  mpteqb  5184  fvmptf  5186  eqfnfv2f  5192  dff13f  5332  ovmpt2s  5545  ov2gf  5546  ovmpt2dxf  5547  ovmpt2df  5553  eqerlem  6046
  Copyright terms: Public domain W3C validator