Theorem nfeq 2912

Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Hypotheses

Ref	Expression
nfnfc.1	⊢ Ⅎ𝑥𝐴
nfeq.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq	⊢ Ⅎ𝑥 𝐴 = 𝐵

Proof of Theorem nfeq

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfeq.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
5	2, 4	nfeqd 2909	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
6	5	mptru 1549	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1542  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2728  df-nfc 2885

This theorem is referenced by:  nfeq1  2914  nfeq2  2916  nfne  3033  raleqf  3318  rmoeq1f  3379  rabeqf  3423  csbhypf  3865  sbceqg  4352  nffn  6597  nffo  6751  fvmptd3f  6963  mpteqb  6967  fvmptf  6969  eqfnfv2f  6987  dff13f  7210  ovmpos  7515  ov2gf  7516  ovmpodxf  7517  ovmpodf  7523  eqerlem  8679  seqof2  14022  sumeq2ii  15655  sumss  15686  fsumadd  15702  fsummulc2  15746  fsumrelem  15770  prodeq1f  15871  prodeq2ii  15876  fprodmul  15925  fproddiv  15926  txcnp  23585  ptcnplem  23586  cnmpt11  23628  cnmpt21  23636  cnmptcom  23643  mbfeqalem1  25608  mbflim  25635  itgeq1f  25738  itgeq1fOLD  25739  itgeqa  25781  dvmptfsum  25942  ulmss  26362  leibpi  26906  o1cxp  26938  lgseisenlem2  27339  nosupbnd1  27678  2ndresdju  32722  aciunf1lem  32735  deg1prod  33643  sigapildsys  34306  bnj1316  34962  bnj1446  35187  bnj1447  35188  bnj1448  35189  bnj1519  35207  bnj1520  35208  bnj1529  35212  subtr  36496  subtr2  36497  bj-sbeqALT  37207  poimirlem25  37966  iuneq2f  38477  mpobi123f  38483  mptbi12f  38487  dvdsrabdioph  43238  fphpd  43244  mnringmulrcld  44655  fvelrnbf  45449  refsum2cnlem1  45468  elrnmpt1sf  45619  choicefi  45629  axccdom  45651  uzublem  45858  fsumf1of  46004  fmuldfeq  46013  mccl  46028  climmulf  46034  climexp  46035  climsuse  46038  climrecf  46039  climaddf  46045  mullimc  46046  neglimc  46075  addlimc  46076  0ellimcdiv  46077  climeldmeqmpt  46096  climfveqmpt  46099  climfveqf  46108  climfveqmpt3  46110  climeldmeqf  46111  climeqf  46116  climeldmeqmpt3  46117  limsupubuzlem  46140  limsupequz  46151  dvnmptdivc  46366  dvmptfprod  46373  stoweidlem18  46446  stoweidlem31  46459  stoweidlem55  46483  stoweidlem59  46487  sge0iunmpt  46846  sge0reuz  46875  iundjiun  46888  hoicvrrex  46984  ovnhoilem1  47029  ovnlecvr2  47038  opnvonmbllem1  47060  vonioo  47110  vonicc  47113  sssmf  47166  smflim  47205  smfpimcclem  47235  smfpimcc  47236  cfsetsnfsetf  47506  ovmpordxf  48815