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

Theorem raleq 3051
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 2616 . 2  |-  F/_ x A
2 nfcv 2616 . 2  |-  F/_ x B
31, 2raleqf 3047 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 1398   A.wral 2804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2809
This theorem is referenced by:  raleqi  3055  raleqdv  3057  raleqbi1dv  3059  sbralie  3094  r19.2zb  3907  inteq  4274  iineq1  4330  reusv6OLD  4648  reusv7OLD  4649  fri  4830  frsn  5059  fncnv  5634  isoeq4  6193  onminex  6615  tfinds  6667  f1oweALT  6757  frxp  6883  tfrlem1  7037  tfrlem12  7050  omeulem1  7223  ixpeq1  7473  undifixp  7498  ac6sfi  7756  frfi  7757  iunfi  7800  indexfi  7820  supeq1  7896  supeq2  7899  bnd2  8302  acneq  8415  aceq3lem  8492  dfac5lem4  8498  dfac8  8506  dfac9  8507  kmlem1  8521  kmlem10  8530  kmlem13  8533  cfval  8618  axcc2lem  8807  axcc4dom  8812  axdc3lem3  8823  axdc3lem4  8824  ac4c  8847  ac5  8848  ac6sg  8859  zorn2lem7  8873  xrsupsslem  11501  xrinfmsslem  11502  xrsupss  11503  xrinfmss  11504  fsuppmapnn0fiubex  12083  rexanuz  13263  rexfiuz  13265  modfsummod  13693  gcdcllem3  14238  isprs  15761  drsdirfi  15769  isdrs2  15770  ispos  15778  lubeldm  15813  lubval  15816  glbeldm  15826  glbval  15829  istos  15867  pospropd  15966  isdlat  16025  mhmpropd  16174  isghm  16469  cntzval  16561  efgval  16937  iscmn  17007  dfrhm2  17564  lidldvgen  18101  coe1fzgsumd  18542  evl1gsumd  18591  ocvval  18874  isobs  18927  mat0dimcrng  19142  mdetunilem9  19292  ist0  19991  cmpcovf  20061  is1stc  20111  2ndc1stc  20121  isref  20179  txflf  20676  ustuqtop4  20916  iscfilu  20960  ispsmet  20977  ismet  20995  isxmet  20996  cncfval  21561  lebnumlem3  21632  fmcfil  21880  iscfil3  21881  caucfil  21891  iscmet3  21901  cfilres  21904  minveclem3  22013  ovolfiniun  22081  finiunmbl  22123  volfiniun  22126  dvcn  22493  ulmval  22944  axtgcont1  24066  nb3grapr  24658  rusgrasn  25150  isplig  25384  isgrpo  25399  isablo  25486  isexid2  25528  ismndo2  25548  rngomndo  25624  ocval  26399  acunirnmpt  27729  isomnd  27928  isorng  28027  ismbfm  28463  isanmbfm  28467  derangval  28878  setinds  29453  dfon2lem3  29460  dfon2lem7  29464  tfisg  29527  poseq  29576  wfrlem1  29586  wfrlem15  29600  frrlem1  29630  sltval2  29659  sltres  29667  nodense  29692  nobndup  29703  nobnddown  29704  nofulllem1  29705  dfrdg4  29831  tfrqfree  29832  finixpnum  30281  mblfinlem1  30294  mbfresfi  30304  isfne  30400  indexdom  30468  heibor1lem  30548  pridl  30677  smprngopr  30692  ispridlc  30710  setindtrs  31209  dford3lem2  31211  dfac11  31250  fnchoice  31647  raleqd  31683  stoweidlem31  32055  stoweidlem57  32081  fourierdlem80  32211  fourierdlem103  32234  fourierdlem104  32235  mgmhmpropd  32864  rnghmval  32970  zrrnghm  32996  bnj865  34401  bnj1154  34475  bnj1296  34497  bnj1463  34531
  Copyright terms: Public domain W3C validator