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

Theorem nfeq 2168
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 2017 . 2 (A = Bz(z Az B))
2 nfnfc.1 . . . . 5 xA
32nfcri 2155 . . . 4 x z A
4 nfeq.2 . . . . 5 xB
54nfcri 2155 . . . 4 x z B
63, 5nfbi 1465 . . 3 x(z Az B)
76nfal 1452 . 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 1375  wnfc 2148
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 1364  ax-ie2 1365  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-tru 1231  df-nf 1330  df-sb 1629  df-cleq 2016  df-clel 2019  df-nfc 2150
This theorem is referenced by:  nfel  2169  nfeq1  2170  nfeq2  2172  nfne  2274  raleqf  2478  rexeqf  2479  reueq1f  2480  rmoeq1f  2481  rabeqf  2527  sbceqg  2842  csbhypf  2861  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  6043
  Copyright terms: Public domain W3C validator