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

Theorem nfeq 2640
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 2636 . 2  |-  ( T. 
->  F/ x  A  =  B )
65trud 1388 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   T. wtru 1380   F/wnf 1599   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-nfc 2617
This theorem is referenced by:  nfelOLD  2643  nfeq1  2644  nfeq2  2646  nfne  2798  raleqf  3054  rexeqf  3055  reueq1f  3056  rmoeq1f  3057  rabeqf  3106  csbhypf  3454  sbceqg  3825  nffn  5677  nffo  5794  fvmptdf  5961  mpteqb  5964  fvmptf  5966  eqfnfv2f  5979  dff13f  6155  ovmpt2s  6410  ov2gf  6411  ovmpt2dxf  6412  ovmpt2df  6418  eqerlem  7343  seqof2  12133  sumeq2w  13477  sumeq2ii  13478  sumss  13509  fsumadd  13524  fsummulc2  13562  fsumrelem  13584  txcnp  19884  ptcnplem  19885  cnmpt11  19927  cnmpt21  19935  cnmptcom  19942  mbfeqalem  21812  mbflim  21838  itgeq1f  21941  itgeqa  21983  dvmptfsum  22139  ulmss  22554  leibpi  23029  o1cxp  23060  lgseisenlem2  23381  istrkg2ld  23614  disjunsn  27154  opabdm  27165  opabrn  27166  mpt2mptxf  27218  f1od2  27247  fpwrelmap  27256  oms0  27934  prodeq1f  28645  prodeq2w  28649  prodeq2ii  28650  fprodmul  28695  fproddiv  28696  subtr  29737  subtr2  29738  iuneq2f  30195  mpt2bi123f  30203  mptbi12f  30207  dvdsrabdioph  30375  fphpd  30382  fvelrnbf  30999  refsum2cnlem1  31018  fmuldfeq  31161  climmulf  31174  climexp  31175  climsuse  31178  climrecf  31179  climaddf  31185  mullimc  31186  climf  31192  neglimc  31217  addlimc  31218  0ellimcdiv  31219  cncficcgt0  31255  cncfiooicclem1  31260  stoweidlem18  31346  stoweidlem31  31359  stoweidlem55  31383  stoweidlem59  31387  fourierdlem80  31515  ovmpt2rdxf  32024  bnj1316  32976  bnj1446  33198  bnj1447  33199  bnj1448  33200  bnj1519  33218  bnj1520  33219  bnj1529  33223  bj-sbeqALT  33566
  Copyright terms: Public domain W3C validator