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

Theorem nfeq 2626
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 2623 . 2  |-  ( T. 
->  F/ x  A  =  B )
65trud 1379 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   T. wtru 1371   F/wnf 1590   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-cleq 2446  df-nfc 2604
This theorem is referenced by:  nfelOLD  2629  nfeq1  2630  nfeq2  2632  nfne  2782  raleqf  3017  rexeqf  3018  reueq1f  3019  rmoeq1f  3020  rabeqf  3069  csbhypf  3413  sbceqg  3784  nffn  5614  nffo  5726  fvmptdf  5893  mpteqb  5896  fvmptf  5898  eqfnfv2f  5909  dff13f  6081  ovmpt2s  6323  ov2gf  6324  ovmpt2dxf  6325  ovmpt2df  6331  eqerlem  7242  seqof2  11980  sumeq2w  13286  sumeq2ii  13287  sumss  13318  fsumadd  13332  fsummulc2  13368  fsumrelem  13387  txcnp  19324  ptcnplem  19325  cnmpt11  19367  cnmpt21  19375  cnmptcom  19382  mbfeqalem  21252  mbflim  21278  itgeq1f  21381  itgeqa  21423  dvmptfsum  21579  ulmss  21994  leibpi  22469  o1cxp  22500  lgseisenlem2  22821  istrkg2ld  23054  disjunsn  26086  opabdm  26093  opabrn  26094  mpt2mptxf  26145  f1od2  26174  fpwrelmap  26183  oms0  26853  prodeq1f  27564  prodeq2w  27568  prodeq2ii  27569  fprodmul  27614  fproddiv  27615  subtr  28656  subtr2  28657  iuneq2f  29114  mpt2bi123f  29122  mptbi12f  29126  dvdsrabdioph  29295  fphpd  29302  fvelrnbf  29887  refsum2cnlem1  29906  fmuldfeq  29911  climmulf  29924  climexp  29925  climsuse  29928  climrecf  29929  stoweidlem18  29960  stoweidlem31  29973  stoweidlem55  29997  stoweidlem59  30001  ovmpt2rdxf  30876  bnj1316  32131  bnj1446  32353  bnj1447  32354  bnj1448  32355  bnj1519  32373  bnj1520  32374  bnj1529  32378  bj-sbeqALT  32719
  Copyright terms: Public domain W3C validator