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

Theorem nfeq2 2171
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1 xB
Assertion
Ref Expression
nfeq2 x A = B
Distinct variable group:   x,A
Allowed substitution hint:   B(x)

Proof of Theorem nfeq2
StepHypRef Expression
1 nfcv 2160 . 2 xA
2 nfeq2.1 . 2 xB
31, 2nfeq 2167 1 x A = B
Colors of variables: wff set class
Syntax hints:   = wceq 1228  wnf 1329  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:  issetf  2540  eqvincf  2646  csbhypf  2862  nfpr  3394  intab  3618  nfmpt  3823  cbvmpt  3825  repizf2  3889  moop2  3962  eusvnf  4135  elrnmpt1  4512  fmptco  5255  elabrex  5322  nfmpt2  5496  cbvmpt2x  5505  ovmpt2dxf  5549  fmpt2x  5749  nfrecs  5844  erovlem  6109
  Copyright terms: Public domain W3C validator