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

Theorem raleq 3058
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Assertion
Ref Expression
raleq  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem raleq
StepHypRef Expression
1 nfcv 2629 . 2  |-  F/_ x A
2 nfcv 2629 . 2  |-  F/_ x B
31, 2raleqf 3054 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819
This theorem is referenced by:  raleqi  3062  raleqdv  3064  raleqbi1dv  3066  sbralie  3101  r19.2zb  3918  inteq  4285  iineq1  4340  reusv6OLD  4658  reusv7OLD  4659  fri  4841  frsn  5069  fncnv  5650  isoeq4  6204  onminex  6620  tfinds  6672  f1oweALT  6765  frxp  6890  tfrlem1  7042  tfrlem12  7055  omeulem1  7228  ixpeq1  7477  undifixp  7502  ac6sfi  7760  frfi  7761  iunfi  7804  indexfi  7824  supeq1  7901  supeq2  7904  bnd2  8307  acneq  8420  aceq3lem  8497  dfac5lem4  8503  dfac8  8511  dfac9  8512  kmlem1  8526  kmlem10  8535  kmlem13  8538  cfval  8623  axcc2lem  8812  axcc4dom  8817  axdc3lem3  8828  axdc3lem4  8829  ac4c  8852  ac5  8853  ac6sg  8864  zorn2lem7  8878  xrsupsslem  11494  xrinfmsslem  11495  xrsupss  11496  xrinfmss  11497  fsuppmapnn0fiubex  12062  rexanuz  13137  rexfiuz  13139  modfsummod  13567  gcdcllem3  14006  isprs  15413  drsdirfi  15421  isdrs2  15422  ispos  15430  lubeldm  15464  lubval  15467  glbeldm  15477  glbval  15480  istos  15518  pospropd  15617  isdlat  15676  mhmpropd  15783  isghm  16062  cntzval  16154  efgval  16531  iscmn  16601  dfrhm2  17150  lidldvgen  17685  coe1fzgsumd  18115  evl1gsumd  18164  ocvval  18465  isobs  18518  mat0dimcrng  18739  mdetunilem9  18889  ist0  19587  cmpcovf  19657  is1stc  19708  2ndc1stc  19718  txflf  20242  ustuqtop4  20482  iscfilu  20526  ispsmet  20543  ismet  20561  isxmet  20562  cncfval  21127  lebnumlem3  21198  fmcfil  21446  iscfil3  21447  caucfil  21457  iscmet3  21467  cfilres  21470  minveclem3  21579  ovolfiniun  21647  finiunmbl  21689  volfiniun  21692  dvcn  22059  ulmval  22509  istrkgld  23585  axtgcont1  23593  nb3grapr  24129  rusgrasn  24621  isplig  24855  isgrpo  24874  isablo  24961  isexid2  25003  ismndo2  25023  rngomndo  25099  ocval  25874  isomnd  27353  isorng  27452  ismbfm  27863  isanmbfm  27867  derangval  28251  setinds  28787  dfon2lem3  28794  dfon2lem7  28798  tfisg  28861  poseq  28910  wfrlem1  28920  wfrlem15  28934  frrlem1  28964  sltval2  28993  sltres  29001  nodense  29026  nobndup  29037  nobnddown  29038  nofulllem1  29039  dfrdg4  29177  tfrqfree  29178  finixpnum  29615  mblfinlem1  29628  mbfresfi  29638  isfne  29740  isref  29751  indexdom  29828  heibor1lem  29908  pridl  30037  smprngopr  30052  ispridlc  30070  setindtrs  30571  dford3lem2  30573  dfac11  30612  fnchoice  30982  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem31  31331  stoweidlem57  31357  fourierdlem45  31452  fourierdlem70  31477  fourierdlem71  31478  fourierdlem80  31487  fourierdlem103  31510  fourierdlem104  31511  bnj865  33060  bnj1154  33134  bnj1296  33156  bnj1463  33190
  Copyright terms: Public domain W3C validator