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

Theorem nfeq 2593
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  |-  F/_ x A
nfeq.2  |-  F/_ x B
Assertion
Ref Expression
nfeq  |-  F/ x  A  =  B

Proof of Theorem nfeq
StepHypRef Expression
1 nfnfc.1 . . . 4  |-  F/_ x A
21a1i 11 . . 3  |-  ( T. 
->  F/_ x A )
3 nfeq.2 . . . 4  |-  F/_ x B
43a1i 11 . . 3  |-  ( T. 
->  F/_ x B )
52, 4nfeqd 2589 . 2  |-  ( T. 
->  F/ x  A  =  B )
65trud 1446 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   T. wtru 1438   F/wnf 1663   F/_wnfc 2568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2412  df-nfc 2570
This theorem is referenced by:  nfelOLD  2596  nfeq1  2597  nfeq2  2599  nfne  2754  raleqf  3019  rexeqf  3020  reueq1f  3021  rmoeq1f  3022  rabeqf  3071  csbhypf  3411  sbceqg  3798  nffn  5681  nffo  5800  fvmptdf  5968  mpteqb  5971  fvmptf  5973  eqfnfv2f  5986  dff13f  6166  ovmpt2s  6425  ov2gf  6426  ovmpt2dxf  6427  ovmpt2df  6433  eqerlem  7394  seqof2  12257  sumeq2ii  13726  sumss  13757  fsumadd  13772  fsummulc2  13812  fsumrelem  13834  prodeq1f  13929  prodeq2ii  13934  fprodmul  13981  fproddiv  13982  fprodle  14017  txcnp  20559  ptcnplem  20560  cnmpt11  20602  cnmpt21  20610  cnmptcom  20617  mbfeqalem  22492  mbflim  22520  itgeq1f  22623  itgeqa  22665  dvmptfsum  22821  ulmss  23243  leibpi  23759  o1cxp  23791  lgseisenlem2  24167  fmptcof2  28125  aciunf1lem  28130  sigapildsys  28849  oms0  28984  bnj1316  29446  bnj1446  29668  bnj1447  29669  bnj1448  29670  bnj1519  29688  bnj1520  29689  bnj1529  29693  subtr  30781  subtr2  30782  bj-sbeqALT  31278  poimirlem25  31698  iuneq2f  32131  mpt2bi123f  32139  mptbi12f  32143  dvdsrabdioph  35391  fphpd  35397  fvelrnbf  37012  refsum2cnlem1  37031  dffo3f  37106  elrnmptf  37110  disjrnmpt2  37119  disjinfi  37124  fsumf1of  37261  fmuldfeq  37266  mccl  37283  climmulf  37287  climexp  37288  climsuse  37292  climrecf  37293  climaddf  37300  mullimc  37301  neglimc  37333  addlimc  37334  0ellimcdiv  37335  dvnmptdivc  37415  dvmptfprod  37422  dvnprodlem1  37423  stoweidlem18  37480  stoweidlem31  37494  stoweidlem55  37518  stoweidlem59  37522  sge0f1o  37791  sge0iunmpt  37827  iundjiun  37840  ovmpt2rdxf  38922
  Copyright terms: Public domain W3C validator