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

Theorem nfeq 2623
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 2619 . 2  |-  ( T. 
->  F/ x  A  =  B )
65trud 1461 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1452   T. wtru 1453   F/wnf 1675   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-cleq 2464  df-nfc 2601
This theorem is referenced by:  nfeq1  2625  nfeq2  2627  nfne  2742  raleqf  2969  rexeqf  2970  reueq1f  2971  rmoeq1f  2972  rabeqf  3023  csbhypf  3368  sbceqg  3777  nffn  5682  nffo  5805  fvmptdf  5976  mpteqb  5979  fvmptf  5981  eqfnfv2f  5995  dff13f  6178  ovmpt2s  6439  ov2gf  6440  ovmpt2dxf  6441  ovmpt2df  6447  eqerlem  7413  seqof2  12309  sumeq2ii  13836  sumss  13867  fsumadd  13882  fsummulc2  13922  fsumrelem  13944  prodeq1f  14039  prodeq2ii  14044  fprodmul  14091  fproddiv  14092  fprodle  14127  txcnp  20712  ptcnplem  20713  cnmpt11  20755  cnmpt21  20763  cnmptcom  20770  mbfeqalem  22677  mbflim  22705  itgeq1f  22808  itgeqa  22850  dvmptfsum  23006  ulmss  23431  leibpi  23947  o1cxp  23979  lgseisenlem2  24357  fmptcof2  28334  aciunf1lem  28339  sigapildsys  29058  oms0OLD  29202  bnj1316  29704  bnj1446  29926  bnj1447  29927  bnj1448  29928  bnj1519  29946  bnj1520  29947  bnj1529  29951  subtr  31041  subtr2  31042  bj-sbeqALT  31570  poimirlem25  32029  iuneq2f  32462  mpt2bi123f  32470  mptbi12f  32474  dvdsrabdioph  35724  fphpd  35730  fvelrnbf  37402  refsum2cnlem1  37421  dffo3f  37521  elrnmptf  37525  disjrnmpt2  37534  disjinfi  37539  choicefi  37552  fsumf1of  37749  fmuldfeq  37758  mccl  37775  climmulf  37779  climexp  37780  climsuse  37784  climrecf  37785  climaddf  37792  mullimc  37793  neglimc  37825  addlimc  37826  0ellimcdiv  37827  dvnmptdivc  37910  dvmptfprod  37917  dvnprodlem1  37918  stoweidlem18  37990  stoweidlem31  38004  stoweidlem55  38028  stoweidlem59  38032  sge0f1o  38338  sge0iunmpt  38374  iundjiun  38414  hoicvrrex  38496  ovnhoilem1  38541  ovnlecvr2  38550  opnvonmbllem1  38572  ovmpt2rdxf  40628
  Copyright terms: Public domain W3C validator