Theorem nfeq2 2294

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

Step	Hyp	Ref	Expression
1		nfcv 2282	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2290	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1332  Ⅎwnf 1437  Ⅎwnfc 2269

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-cleq 2133  df-clel 2136  df-nfc 2271

This theorem is referenced by:  issetf  2696  eqvincf  2814  csbhypf  3043  nfpr  3581  intab  3808  nfmpt  4028  cbvmptf  4030  cbvmpt  4031  repizf2  4094  moop2  4181  eusvnf  4382  elrnmpt1  4798  fmptco  5594  elabrex  5667  nfmpo  5848  cbvmpox  5857  ovmpodxf  5904  fmpox  6106  f1od2  6140  nfrecs  6212  erovlem  6529  xpf1o  6746  mapxpen  6750  mkvprop  7040  cc3  7100  lble  8729  nfsum1  11157  nfsum  11158  zsumdc  11185  fsum3  11188  fsum3cvg2  11195  fsum2dlemstep  11235  mertenslem2  11337  nfcprod1  11355  nfcprod  11356  zproddc  11380  ctiunctlemfo  11988  ellimc3apf  12837