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

Theorem nfeq 2427
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 2278 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2414 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2414 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1774 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1768 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1557 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527   F/wnf 1531    = wceq 1623    e. wcel 1685   F/_wnfc 2407
This theorem is referenced by:  nfel  2428  nfeq1  2429  nfeq2  2431  nfne  2540  raleqf  2733  rexeqf  2734  reueq1f  2735  rmoeq1f  2736  rabeqf  2782  sbceqg  3098  csbhypf  3117  nffn  5306  nffo  5416  fvmptdf  5573  mpteqb  5576  fvmptf  5578  eqfnfv2f  5588  dff13f  5746  ovmpt2s  5933  ov2gf  5934  ovmpt2dxf  5935  ovmpt2df  5941  opabiota  6287  eqerlem  6688  sumeq1f  12157  sumeq2w  12161  sumeq2ii  12162  sumss  12193  fsumadd  12207  fsummulc2  12242  fsumrelem  12261  txcnp  17310  ptcnplem  17311  cnmpt11  17353  cnmpt21  17361  cnmptcom  17368  mbfeqalem  18993  mbflim  19019  itgeq1f  19122  itgeqa  19164  dvmptfsum  19318  ulmss  19770  leibpi  20234  o1cxp  20265  lgseisenlem2  20585  dfimafnf  23037  prodeq3ii  24719  fprodadd  24763  fprodneg  24789  fprodsub  24790  subtr  25635  subtr2  25636  dvdsrabdioph  26302  fphpd  26310  fvelrnbf  27100  refsum2cnlem1  27119  fmuldfeqlem1  27123  fmuldfeq  27124  climmulf  27141  climexp  27142  climsuse  27145  climrecf  27146  stoweidlem8  27168  stoweidlem16  27176  stoweidlem18  27178  stoweidlem19  27179  stoweidlem21  27181  stoweidlem22  27182  stoweidlem23  27183  stoweidlem28  27188  stoweidlem29  27189  stoweidlem31  27191  stoweidlem32  27192  stoweidlem35  27195  stoweidlem36  27196  stoweidlem41  27201  stoweidlem44  27204  stoweidlem45  27205  stoweidlem48  27208  stoweidlem51  27211  stoweidlem53  27213  stoweidlem55  27215  stoweidlem58  27218  stoweidlem59  27219  stoweidlem60  27220  bnj1316  28132  bnj1446  28354  bnj1447  28355  bnj1448  28356  bnj1519  28374  bnj1520  28375  bnj1529  28379
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-cleq 2277  df-clel 2280  df-nfc 2409
  Copyright terms: Public domain W3C validator