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

Theorem nfeq 2547
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
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
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2398 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2534 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2534 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1852 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1860 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1576 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546   F/wnf 1550    = wceq 1649    e. wcel 1721   F/_wnfc 2527
This theorem is referenced by:  nfel  2548  nfeq1  2549  nfeq2  2551  nfne  2658  raleqf  2860  rexeqf  2861  reueq1f  2862  rmoeq1f  2863  rabeqf  2909  sbceqg  3227  csbhypf  3246  nffn  5500  nffo  5611  fvmptdf  5775  mpteqb  5778  fvmptf  5780  eqfnfv2f  5790  dff13f  5965  ovmpt2s  6156  ov2gf  6157  ovmpt2dxf  6158  ovmpt2df  6164  eqerlem  6896  seqof2  11336  sumeq1f  12437  sumeq2w  12441  sumeq2ii  12442  sumss  12473  fsumadd  12487  fsummulc2  12522  fsumrelem  12541  txcnp  17605  ptcnplem  17606  cnmpt11  17648  cnmpt21  17656  cnmptcom  17663  mbfeqalem  19487  mbflim  19513  itgeq1f  19616  itgeqa  19658  dvmptfsum  19812  ulmss  20266  leibpi  20735  o1cxp  20766  lgseisenlem2  21087  prodeq1f  25187  prodeq2w  25191  prodeq2ii  25192  fprodmul  25237  fproddiv  25238  subtr  26207  subtr2  26208  dvdsrabdioph  26760  fphpd  26767  fvelrnbf  27556  refsum2cnlem1  27575  fmuldfeq  27580  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  stoweidlem18  27634  stoweidlem31  27647  stoweidlem55  27671  stoweidlem59  27675  bnj1316  28898  bnj1446  29120  bnj1447  29121  bnj1448  29122  bnj1519  29140  bnj1520  29141  bnj1529  29145
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529
  Copyright terms: Public domain W3C validator