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

Theorem nfeq 2761
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 2757 . 2 (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
65trud 1483 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wtru 1475  wnf 1698  wnfc 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-nfc 2739
This theorem is referenced by:  nfeq1  2763  nfeq2  2765  nfne  2881  raleqf  3110  rexeqf  3111  reueq1f  3112  rmoeq1f  3113  rabeqf  3164  csbhypf  3517  sbceqg  3935  nffn  5887  nffo  6012  fvmptdf  6189  mpteqb  6192  fvmptf  6194  eqfnfv2f  6208  dff13f  6395  ovmpt2s  6660  ov2gf  6661  ovmpt2dxf  6662  ovmpt2df  6668  eqerlem  7640  seqof2  12676  sumeq2ii  14217  sumss  14248  fsumadd  14263  fsummulc2  14304  fsumrelem  14326  prodeq1f  14423  prodeq2ii  14428  fprodmul  14475  fproddiv  14476  fprodle  14512  txcnp  21175  ptcnplem  21176  cnmpt11  21218  cnmpt21  21226  cnmptcom  21233  mbfeqalem  23132  mbflim  23158  itgeq1f  23261  itgeqa  23303  dvmptfsum  23459  ulmss  23872  leibpi  24386  o1cxp  24418  lgseisenlem2  24818  fmptcof2  28645  aciunf1lem  28650  sigapildsys  29358  bnj1316  29951  bnj1446  30173  bnj1447  30174  bnj1448  30175  bnj1519  30193  bnj1520  30194  bnj1529  30198  subtr  31284  subtr2  31285  bj-sbeqALT  31883  poimirlem25  32400  iuneq2f  32929  mpt2bi123f  32937  mptbi12f  32941  dvdsrabdioph  36188  fphpd  36194  fvelrnbf  37996  refsum2cnlem1  38015  dffo3f  38155  elrnmptf  38158  disjrnmpt2  38166  disjinfi  38171  choicefi  38183  axccdom  38207  fsumf1of  38438  fmuldfeq  38447  mccl  38462  climmulf  38468  climexp  38469  climsuse  38472  climrecf  38473  climaddf  38479  mullimc  38480  neglimc  38511  addlimc  38512  0ellimcdiv  38513  climeldmeqmpt  38532  climfveqmpt  38535  dvnmptdivc  38625  dvmptfprod  38632  dvnprodlem1  38633  stoweidlem18  38708  stoweidlem31  38721  stoweidlem55  38745  stoweidlem59  38749  sge0f1o  39072  sge0iunmpt  39108  sge0reuz  39137  iundjiun  39150  hoicvrrex  39243  ovnhoilem1  39288  ovnlecvr2  39297  opnvonmbllem1  39319  vonioo  39370  vonicc  39373  sssmf  39422  smflim  39460  ovmpt2rdxf  41905
  Copyright terms: Public domain W3C validator