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

Theorem nfeq 2925
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 2921 . 2 (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
65trud 1641 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wtru 1632  wnf 1856  wnfc 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-nfc 2902
This theorem is referenced by:  nfeq1  2927  nfeq2  2929  nfne  3043  raleqf  3283  rexeqf  3284  reueq1f  3285  rmoeq1f  3286  rabeqf  3340  csbhypf  3702  sbceqg  4129  nffn  6128  nffo  6256  fvmptd3f  6438  mpteqb  6442  fvmptf  6444  eqfnfv2f  6459  dff13f  6657  ovmpt2s  6932  ov2gf  6933  ovmpt2dxf  6934  ovmpt2df  6940  eqerlem  7931  seqof2  13067  sumeq2ii  14632  sumss  14664  fsumadd  14679  fsummulc2  14724  fsumrelem  14747  prodeq1f  14846  prodeq2ii  14851  fprodmul  14898  fproddiv  14899  fprodle  14934  txcnp  21645  ptcnplem  21646  cnmpt11  21688  cnmpt21  21696  cnmptcom  21703  mbfeqalem  23630  mbflim  23656  itgeq1f  23759  itgeqa  23801  dvmptfsum  23959  ulmss  24372  leibpi  24891  o1cxp  24923  lgseisenlem2  25323  fmptcof2  29798  aciunf1lem  29803  sigapildsys  30566  bnj1316  31230  bnj1446  31452  bnj1447  31453  bnj1448  31454  bnj1519  31472  bnj1520  31473  bnj1529  31477  nosupbnd1  32198  subtr  32646  subtr2  32647  bj-sbeqALT  33225  poimirlem25  33768  iuneq2f  34296  mpt2bi123f  34304  mptbi12f  34308  dvdsrabdioph  37901  fphpd  37907  fvelrnbf  39700  refsum2cnlem1  39719  dffo3f  39885  elrnmptf  39888  disjrnmpt2  39896  disjinfi  39901  choicefi  39911  axccdom  39935  fvelimad  39977  uzublem  40174  fsumf1of  40325  fmuldfeq  40334  mccl  40349  climmulf  40355  climexp  40356  climsuse  40359  climrecf  40360  climaddf  40366  mullimc  40367  neglimc  40398  addlimc  40399  0ellimcdiv  40400  climeldmeqmpt  40419  climfveqmpt  40422  climfveqf  40431  climfveqmpt3  40433  climeldmeqf  40434  climeqf  40439  climeldmeqmpt3  40440  limsupubuzlem  40463  limsupequz  40474  dvnmptdivc  40672  dvmptfprod  40679  dvnprodlem1  40680  stoweidlem18  40753  stoweidlem31  40766  stoweidlem55  40790  stoweidlem59  40794  sge0f1o  41117  sge0iunmpt  41153  sge0reuz  41182  iundjiun  41195  hoicvrrex  41291  ovnhoilem1  41336  ovnlecvr2  41345  opnvonmbllem1  41367  vonioo  41417  vonicc  41420  sssmf  41468  smflim  41506  smfpimcclem  41534  smfpimcc  41535  ovmpt2rdxf  42646
  Copyright terms: Public domain W3C validator