MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeq Structured version   Visualization version   GIF version

Theorem nfeq 2772
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
StepHypRef Expression
1 nfnfc.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
3 nfeq.2 . . . 4 𝑥𝐵
43a1i 11 . . 3 (⊤ → 𝑥𝐵)
52, 4nfeqd 2768 . 2 (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
65trud 1490 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wtru 1481  wnf 1705  wnfc 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-nfc 2750
This theorem is referenced by:  nfeq1  2774  nfeq2  2776  nfne  2890  raleqf  3123  rexeqf  3124  reueq1f  3125  rmoeq1f  3126  rabeqf  3178  csbhypf  3533  sbceqg  3956  nffn  5945  nffo  6071  fvmptdf  6252  mpteqb  6255  fvmptf  6257  eqfnfv2f  6271  dff13f  6467  ovmpt2s  6737  ov2gf  6738  ovmpt2dxf  6739  ovmpt2df  6745  eqerlem  7721  seqof2  12799  sumeq2ii  14357  sumss  14388  fsumadd  14403  fsummulc2  14444  fsumrelem  14466  prodeq1f  14563  prodeq2ii  14568  fprodmul  14615  fproddiv  14616  fprodle  14652  txcnp  21333  ptcnplem  21334  cnmpt11  21376  cnmpt21  21384  cnmptcom  21391  mbfeqalem  23315  mbflim  23341  itgeq1f  23444  itgeqa  23486  dvmptfsum  23642  ulmss  24055  leibpi  24569  o1cxp  24601  lgseisenlem2  25001  fmptcof2  29296  aciunf1lem  29301  sigapildsys  30003  bnj1316  30596  bnj1446  30818  bnj1447  30819  bnj1448  30820  bnj1519  30838  bnj1520  30839  bnj1529  30843  subtr  31947  subtr2  31948  bj-sbeqALT  32539  poimirlem25  33063  iuneq2f  33592  mpt2bi123f  33600  mptbi12f  33604  dvdsrabdioph  36851  fphpd  36857  fvelrnbf  38657  refsum2cnlem1  38676  dffo3f  38835  elrnmptf  38838  disjrnmpt2  38846  disjinfi  38851  choicefi  38863  axccdom  38887  fvelimad  38930  uzublem  39118  fsumf1of  39207  fmuldfeq  39216  mccl  39231  climmulf  39237  climexp  39238  climsuse  39241  climrecf  39242  climaddf  39248  mullimc  39249  neglimc  39280  addlimc  39281  0ellimcdiv  39282  climeldmeqmpt  39301  climfveqmpt  39304  climfveqf  39313  climfveqmpt3  39315  climeldmeqf  39316  climeqf  39321  climeldmeqmpt3  39322  limsupubuzlem  39345  limsupequz  39356  dvnmptdivc  39456  dvmptfprod  39463  dvnprodlem1  39464  stoweidlem18  39539  stoweidlem31  39552  stoweidlem55  39576  stoweidlem59  39580  sge0f1o  39903  sge0iunmpt  39939  sge0reuz  39968  iundjiun  39981  hoicvrrex  40074  ovnhoilem1  40119  ovnlecvr2  40128  opnvonmbllem1  40150  vonioo  40200  vonicc  40203  sssmf  40251  smflim  40289  smfpimcclem  40317  smfpimcc  40318  ovmpt2rdxf  41402
  Copyright terms: Public domain W3C validator