Theorem nfeq2 2909

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 2891	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2905	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1533  Ⅎwnf 1777  Ⅎwnfc 2875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-cleq 2717  df-nfc 2877

This theorem is referenced by:  eqvincf  3633  csbhypf  3918  nfpr  4696  intab  4982  nfmpt  5256  cbvmptf  5258  cbvmptfg  5259  zfrepclf  5295  eusvnf  5392  reusv2lem4  5401  reusv2  5403  moop2  5504  elrnmpt1  5960  opabiota  6980  fvmptdf  7010  dffo3f  7115  fmptco  7138  elabrex  7252  elabrexg  7253  nfmpo  7502  cbvmpox  7513  ovmpodxf  7571  zfrep6  7959  fmpox  8072  nffrecs  8289  nfwrecsOLD  8323  erovlem  8832  xpf1o  9164  mapxpen  9168  wdom2d  9605  cnfcom3clem  9730  scott0  9911  cplem2  9915  infxpenc2lem2  10045  acnlem  10073  fin23lem32  10369  hsmexlem2  10452  axcc3  10463  ac6num  10504  lble  12199  nfsum1  15672  nfsum  15673  zsum  15700  fsum  15702  fsumcvg2  15709  fsum2dlem  15752  infcvgaux1i  15839  nfcprod1  15890  nfcprod  15891  zprod  15917  fprod  15921  fprodser  15929  fprod2dlem  15960  cayleyhamilton1  22838  neiptopreu  23081  xkocnv  23762  istrkg2ld  28336  cnlnadjlem5  31953  chirred  32277  iundisjf  32458  opabdm  32480  opabrn  32481  dfimafnf  32502  fmptcof2  32524  mpomptxf  32545  f1od2  32585  fpwrelmap  32597  elrspunidl  33240  fedgmullem2  33459  esum2dlem  33842  oms0  34048  bnj1468  34608  bnj981  34712  bnj1463  34817  satfv1  35104  iota5f  35449  nfwlim  35549  bj-seex  36531  isbasisrelowllem1  36965  isbasisrelowllem2  36966  exrecfnlem  36989  finxpreclem6  37006  phpreu  37208  matunitlindflem2  37221  poimirlem24  37248  poimirlem25  37249  poimirlem26  37250  poimirlem27  37251  mbfposadd  37271  itg2addnclem  37275  cover2  37319  indexa  37337  riotasvd  38558  cdleme31sn1  39984  cdleme32fva  40040  cdlemk36  40516  elnn0rabdioph  42365  wdom2d2  42598  cbvmpo2  44603  cbvmpo1  44604  elrnmptf  44693  disjrnmpt2  44700  fmuldfeqlem1  45108  climf  45148  climf2  45192  cncficcgt0  45414  stoweidlem8  45534  stoweidlem16  45542  stoweidlem19  45545  stoweidlem21  45547  stoweidlem22  45548  stoweidlem23  45549  stoweidlem29  45555  stoweidlem32  45558  stoweidlem35  45561  stoweidlem36  45562  stoweidlem41  45567  stoweidlem44  45570  stoweidlem45  45571  stoweidlem51  45577  stoweidlem53  45579  stoweidlem60  45586  fourierdlem80  45712  sprsymrelf  46972  cbvmpox2  47585  ovmpordxf  47588  1arymaptfo  47902  2arymaptfo  47913