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

Theorem nfeq 2773
 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 2769 . 2 (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
65trud 1491 1 𝑥 𝐴 = 𝐵
 Colors of variables: wff setvar class Syntax hints:   = wceq 1481  ⊤wtru 1482  Ⅎwnf 1706  Ⅎwnfc 2749 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-ext 2600 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-cleq 2613  df-nfc 2751 This theorem is referenced by:  nfeq1  2775  nfeq2  2777  nfne  2891  raleqf  3129  rexeqf  3130  reueq1f  3131  rmoeq1f  3132  rabeqf  3185  csbhypf  3545  sbceqg  3975  nffn  5975  nffo  6101  fvmptdf  6282  mpteqb  6285  fvmptf  6287  eqfnfv2f  6301  dff13f  6498  ovmpt2s  6769  ov2gf  6770  ovmpt2dxf  6771  ovmpt2df  6777  eqerlem  7761  seqof2  12842  sumeq2ii  14404  sumss  14436  fsumadd  14451  fsummulc2  14497  fsumrelem  14520  prodeq1f  14619  prodeq2ii  14624  fprodmul  14671  fproddiv  14672  fprodle  14708  txcnp  21404  ptcnplem  21405  cnmpt11  21447  cnmpt21  21455  cnmptcom  21462  mbfeqalem  23390  mbflim  23416  itgeq1f  23519  itgeqa  23561  dvmptfsum  23719  ulmss  24132  leibpi  24650  o1cxp  24682  lgseisenlem2  25082  fmptcof2  29430  aciunf1lem  29435  sigapildsys  30199  bnj1316  30865  bnj1446  31087  bnj1447  31088  bnj1448  31089  bnj1519  31107  bnj1520  31108  bnj1529  31112  nosupbnd1  31834  subtr  32283  subtr2  32284  bj-sbeqALT  32870  poimirlem25  33405  iuneq2f  33934  mpt2bi123f  33942  mptbi12f  33946  dvdsrabdioph  37193  fphpd  37199  fvelrnbf  38997  refsum2cnlem1  39016  dffo3f  39180  elrnmptf  39183  disjrnmpt2  39191  disjinfi  39196  choicefi  39208  axccdom  39232  fvelimad  39274  uzublem  39470  fsumf1of  39606  fmuldfeq  39615  mccl  39630  climmulf  39636  climexp  39637  climsuse  39640  climrecf  39641  climaddf  39647  mullimc  39648  neglimc  39679  addlimc  39680  0ellimcdiv  39681  climeldmeqmpt  39700  climfveqmpt  39703  climfveqf  39712  climfveqmpt3  39714  climeldmeqf  39715  climeqf  39720  climeldmeqmpt3  39721  limsupubuzlem  39744  limsupequz  39755  dvnmptdivc  39916  dvmptfprod  39923  dvnprodlem1  39924  stoweidlem18  39998  stoweidlem31  40011  stoweidlem55  40035  stoweidlem59  40039  sge0f1o  40362  sge0iunmpt  40398  sge0reuz  40427  iundjiun  40440  hoicvrrex  40533  ovnhoilem1  40578  ovnlecvr2  40587  opnvonmbllem1  40609  vonioo  40659  vonicc  40662  sssmf  40710  smflim  40748  smfpimcclem  40776  smfpimcc  40777  ovmpt2rdxf  41882
 Copyright terms: Public domain W3C validator