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

Theorem nfeq2 2270
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1 𝑥𝐵
Assertion
Ref Expression
nfeq2 𝑥 𝐴 = 𝐵
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfeq2
StepHypRef Expression
1 nfcv 2258 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2266 1 𝑥 𝐴 = 𝐵
Colors of variables: wff set class
Syntax hints:   = wceq 1316  wnf 1421  wnfc 2245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-cleq 2110  df-clel 2113  df-nfc 2247
This theorem is referenced by:  issetf  2667  eqvincf  2784  csbhypf  3008  nfpr  3543  intab  3770  nfmpt  3990  cbvmptf  3992  cbvmpt  3993  repizf2  4056  moop2  4143  eusvnf  4344  elrnmpt1  4760  fmptco  5554  elabrex  5627  nfmpo  5808  cbvmpox  5817  ovmpodxf  5864  fmpox  6066  f1od2  6100  nfrecs  6172  erovlem  6489  xpf1o  6706  mapxpen  6710  mkvprop  7000  lble  8669  nfsum1  11080  nfsum  11081  zsumdc  11108  fsum3  11111  fsum3cvg2  11118  fsum2dlemstep  11158  mertenslem2  11260  ctiunctlemfo  11863  ellimc3apf  12709
  Copyright terms: Public domain W3C validator