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

Theorem nfeq 2602
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 2598 . 2  |-  ( T. 
->  F/ x  A  =  B )
65trud 1452 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1443   T. wtru 1444   F/wnf 1666   F/_wnfc 2578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-cleq 2443  df-nfc 2580
This theorem is referenced by:  nfeq1  2604  nfeq2  2606  nfne  2722  raleqf  2982  rexeqf  2983  reueq1f  2984  rmoeq1f  2985  rabeqf  3036  csbhypf  3381  sbceqg  3772  nffn  5670  nffo  5790  fvmptdf  5959  mpteqb  5962  fvmptf  5964  eqfnfv2f  5978  dff13f  6158  ovmpt2s  6417  ov2gf  6418  ovmpt2dxf  6419  ovmpt2df  6425  eqerlem  7392  seqof2  12268  sumeq2ii  13752  sumss  13783  fsumadd  13798  fsummulc2  13838  fsumrelem  13860  prodeq1f  13955  prodeq2ii  13960  fprodmul  14007  fproddiv  14008  fprodle  14043  txcnp  20628  ptcnplem  20629  cnmpt11  20671  cnmpt21  20679  cnmptcom  20686  mbfeqalem  22591  mbflim  22619  itgeq1f  22722  itgeqa  22764  dvmptfsum  22920  ulmss  23345  leibpi  23861  o1cxp  23893  lgseisenlem2  24271  fmptcof2  28252  aciunf1lem  28257  sigapildsys  28977  oms0OLD  29122  bnj1316  29625  bnj1446  29847  bnj1447  29848  bnj1448  29849  bnj1519  29867  bnj1520  29868  bnj1529  29872  subtr  30963  subtr2  30964  bj-sbeqALT  31495  poimirlem25  31958  iuneq2f  32391  mpt2bi123f  32399  mptbi12f  32403  dvdsrabdioph  35647  fphpd  35653  fvelrnbf  37333  refsum2cnlem1  37352  dffo3f  37444  elrnmptf  37448  disjrnmpt2  37457  disjinfi  37462  choicefi  37475  fsumf1of  37647  fmuldfeq  37655  mccl  37672  climmulf  37676  climexp  37677  climsuse  37681  climrecf  37682  climaddf  37689  mullimc  37690  neglimc  37722  addlimc  37723  0ellimcdiv  37724  dvnmptdivc  37807  dvmptfprod  37814  dvnprodlem1  37815  stoweidlem18  37872  stoweidlem31  37886  stoweidlem55  37910  stoweidlem59  37914  sge0f1o  38218  sge0iunmpt  38254  iundjiun  38292  hoicvrrex  38372  ovnhoilem1  38417  ovnlecvr2  38426  opnvonmbllem1  38448  ovmpt2rdxf  40107
  Copyright terms: Public domain W3C validator