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

Theorem raleq 2922
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 2584 . 2  |-  F/_ x A
2 nfcv 2584 . 2  |-  F/_ x B
31, 2raleqf 2918 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 1369   A.wral 2720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2436  df-clel 2439  df-nfc 2573  df-ral 2725
This theorem is referenced by:  raleqi  2926  raleqdv  2928  raleqbi1dv  2930  sbralie  2965  r19.2zb  3775  inteq  4136  iineq1  4190  reusv6OLD  4508  reusv7OLD  4509  fri  4687  frsn  4914  fncnv  5487  isoeq4  6018  onminex  6423  tfinds  6475  f1oweALT  6566  frxp  6687  tfrlem1  6840  tfrlem12  6853  omeulem1  7026  ixpeq1  7279  undifixp  7304  ac6sfi  7561  frfi  7562  iunfi  7604  indexfi  7624  supeq1  7700  supeq2  7703  bnd2  8105  acneq  8218  aceq3lem  8295  dfac5lem4  8301  dfac8  8309  dfac9  8310  kmlem1  8324  kmlem10  8333  kmlem13  8336  cfval  8421  axcc2lem  8610  axcc4dom  8615  axdc3lem3  8626  axdc3lem4  8627  ac4c  8650  ac5  8651  ac6sg  8662  zorn2lem7  8676  xrsupsslem  11274  xrinfmsslem  11275  xrsupss  11276  xrinfmss  11277  rexanuz  12838  rexfiuz  12840  gcdcllem3  13702  isprs  15105  drsdirfi  15113  isdrs2  15114  ispos  15122  lubeldm  15156  lubval  15159  glbeldm  15169  glbval  15172  istos  15210  pospropd  15309  isdlat  15368  mhmpropd  15475  isghm  15752  cntzval  15844  efgval  16219  iscmn  16289  dfrhm2  16813  lidldvgen  17342  evl1gsumd  17796  ocvval  18097  isobs  18150  mdetunilem9  18431  ist0  18929  cmpcovf  18999  is1stc  19050  2ndc1stc  19060  txflf  19584  ustuqtop4  19824  iscfilu  19868  ispsmet  19885  ismet  19903  isxmet  19904  cncfval  20469  lebnumlem3  20540  fmcfil  20788  iscfil3  20789  caucfil  20799  iscmet3  20809  cfilres  20812  minveclem3  20921  ovolfiniun  20989  finiunmbl  21030  volfiniun  21033  dvcn  21400  ulmval  21850  axtgcont1  22934  nb3grapr  23366  isplig  23669  isgrpo  23688  isablo  23775  isexid2  23817  ismndo2  23837  rngomndo  23913  ocval  24688  isomnd  26169  isorng  26272  ismbfm  26672  isanmbfm  26676  derangval  27060  setinds  27596  dfon2lem3  27603  dfon2lem7  27607  tfisg  27670  poseq  27719  wfrlem1  27729  wfrlem15  27743  frrlem1  27773  sltval2  27802  sltres  27810  nodense  27835  nobndup  27846  nobnddown  27847  nofulllem1  27848  dfrdg4  27986  tfrqfree  27987  finixpnum  28419  mblfinlem1  28433  mbfresfi  28443  isfne  28545  isref  28556  indexdom  28633  heibor1lem  28713  pridl  28842  smprngopr  28857  ispridlc  28875  setindtrs  29379  dford3lem2  29381  dfac11  29420  fnchoice  29756  stoweidlem31  29831  stoweidlem57  29857  modfsummod  30250  rusgrasn  30562  fsuppmapnn0fiubex  30805  coe1fzgsumd  30843  mat0dimcrng  30871  bnj865  31921  bnj1154  31995  bnj1296  32017  bnj1463  32051
  Copyright terms: Public domain W3C validator