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

Theorem nfeq 2578
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 2429 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2565 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2565 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1856 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1864 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1579 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549   F/wnf 1553    = wceq 1652    e. wcel 1725   F/_wnfc 2558
This theorem is referenced by:  nfel  2579  nfeq1  2580  nfeq2  2582  nfne  2689  raleqf  2892  rexeqf  2893  reueq1f  2894  rmoeq1f  2895  rabeqf  2941  sbceqg  3259  csbhypf  3278  nffn  5533  nffo  5644  fvmptdf  5808  mpteqb  5811  fvmptf  5813  eqfnfv2f  5823  dff13f  5998  ovmpt2s  6189  ov2gf  6190  ovmpt2dxf  6191  ovmpt2df  6197  eqerlem  6929  seqof2  11373  sumeq1f  12474  sumeq2w  12478  sumeq2ii  12479  sumss  12510  fsumadd  12524  fsummulc2  12559  fsumrelem  12578  txcnp  17644  ptcnplem  17645  cnmpt11  17687  cnmpt21  17695  cnmptcom  17702  mbfeqalem  19526  mbflim  19552  itgeq1f  19655  itgeqa  19697  dvmptfsum  19851  ulmss  20305  leibpi  20774  o1cxp  20805  lgseisenlem2  21126  prodeq1f  25226  prodeq2w  25230  prodeq2ii  25231  fprodmul  25276  fproddiv  25277  subtr  26308  subtr2  26309  dvdsrabdioph  26861  fphpd  26868  fvelrnbf  27656  refsum2cnlem1  27675  fmuldfeq  27680  climmulf  27697  climexp  27698  climsuse  27701  climrecf  27702  stoweidlem18  27734  stoweidlem31  27747  stoweidlem55  27771  stoweidlem59  27775  bnj1316  29129  bnj1446  29351  bnj1447  29352  bnj1448  29353  bnj1519  29371  bnj1520  29372  bnj1529  29376
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560
  Copyright terms: Public domain W3C validator