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

Theorem nfeq 2161
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 2010 . 2 (A = Bz(z Az B))
2 nfnfc.1 . . . . 5 xA
32nfcri 2148 . . . 4 x z A
4 nfeq.2 . . . . 5 xB
54nfcri 2148 . . . 4 x z B
63, 5nfbi 1457 . . 3 x(z Az B)
76nfal 1444 . 2 xz(z Az B)
81, 7nfxfr 1339 1 x A = B
Colors of variables: wff set class
Syntax hints:  wb 98  wal 1224   = wceq 1226  wnf 1325   wcel 1369  wnfc 2141
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 614  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1358  ax-ie2 1359  ax-8 1371  ax-10 1372  ax-11 1373  ax-i12 1374  ax-bnd 1375  ax-4 1376  ax-17 1395  ax-i9 1399  ax-ial 1403  ax-i5r 1404  ax-ext 1998
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1622  df-cleq 2009  df-clel 2012  df-nfc 2143
This theorem is referenced by:  nfel  2162  nfeq1  2163  nfeq2  2165  nfne  2269  raleqf  2473  rexeqf  2474  reueq1f  2475  rmoeq1f  2476  rabeqf  2522  sbceqg  2837  csbhypf  2856  nfiotadxy  4788  nffn  4912  nffo  5021  fvmptdf  5174  mpteqb  5177  fvmptf  5179  eqfnfv2f  5185  dff13f  5325  ovmpt2s  5538  ov2gf  5539  ovmpt2dxf  5540  ovmpt2df  5546  eqerlem  6039
  Copyright terms: Public domain W3C validator