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

Theorem raleq 2986
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 2591 . 2  |-  F/_ x A
2 nfcv 2591 . 2  |-  F/_ x B
31, 2raleqf 2982 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1443   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-ext 2430
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ral 2741
This theorem is referenced by:  raleqi  2990  raleqdv  2992  raleqbi1dv  2994  sbralie  3031  r19.2zb  3858  inteq  4236  iineq1  4292  fri  4795  frsn  4904  fncnv  5645  isoeq4  6211  onminex  6631  tfinds  6683  f1oweALT  6774  frxp  6903  wfrlem1  7032  wfrlem15  7047  tfrlem1  7091  tfrlem12  7104  omeulem1  7280  ixpeq1  7530  undifixp  7555  ac6sfi  7812  frfi  7813  iunfi  7859  indexfi  7879  supeq1  7956  supeq2  7959  bnd2  8361  acneq  8471  aceq3lem  8548  dfac5lem4  8554  dfac8  8562  dfac9  8563  kmlem1  8577  kmlem10  8586  kmlem13  8589  cfval  8674  axcc2lem  8863  axcc4dom  8868  axdc3lem3  8879  axdc3lem4  8880  ac4c  8903  ac5  8904  ac6sg  8915  zorn2lem7  8929  xrsupsslem  11589  xrinfmsslem  11590  xrsupss  11591  xrinfmss  11592  fsuppmapnn0fiubex  12201  rexanuz  13401  rexfiuz  13403  modfsummod  13847  gcdcllem3  14468  lcmfval  14584  lcmf0val  14585  lcmfvalOLD  14588  lcmfunsnlem  14607  coprmprod  14671  coprmproddvds  14673  isprs  16168  drsdirfi  16176  isdrs2  16177  ispos  16185  lubeldm  16220  lubval  16223  glbeldm  16233  glbval  16236  istos  16274  pospropd  16373  isdlat  16432  mhmpropd  16581  isghm  16876  cntzval  16968  efgval  17360  iscmn  17430  dfrhm2  17938  lidldvgen  18472  coe1fzgsumd  18889  evl1gsumd  18938  ocvval  19223  isobs  19276  mat0dimcrng  19488  mdetunilem9  19638  ist0  20329  cmpcovf  20399  is1stc  20449  2ndc1stc  20459  isref  20517  txflf  21014  ustuqtop4  21252  iscfilu  21296  ispsmet  21313  ismet  21331  isxmet  21332  cncfval  21913  lebnumlem3  21984  lebnumlem3OLD  21987  fmcfil  22235  iscfil3  22236  caucfil  22246  iscmet3  22256  cfilres  22259  minveclem3  22364  minveclem3OLD  22376  ovolfiniun  22447  finiunmbl  22490  volfiniun  22493  dvcn  22868  ulmval  23328  axtgcont1  24509  tgcgr4  24569  nb3grapr  25174  rusgrasn  25666  isplig  25902  isgrpo  25917  isablo  26004  isexid2  26046  ismndo2  26066  rngomndo  26142  ocval  26926  acunirnmpt  28254  isomnd  28457  isorng  28555  ismbfm  29067  isanmbfm  29071  bnj865  29727  bnj1154  29801  bnj1296  29823  bnj1463  29857  derangval  29883  setinds  30417  dfon2lem3  30424  dfon2lem7  30428  tfisg  30450  poseq  30484  frrlem1  30507  sltval2  30536  sltres  30544  nodense  30571  nobndup  30582  nobnddown  30583  nofulllem1  30584  dfrecs2  30710  dfrdg4  30711  isfne  30988  finixpnum  31923  mblfinlem1  31970  mbfresfi  31980  indexdom  32054  heibor1lem  32134  pridl  32263  smprngopr  32278  ispridlc  32296  setindtrs  35874  dford3lem2  35876  dfac11  35914  fnchoice  37344  stoweidlem31  37886  stoweidlem57  37912  fourierdlem80  38044  fourierdlem103  38067  fourierdlem104  38068  issal  38169  nb3grpr  39439  cplgr0v  39478  mgmhmpropd  39772  rnghmval  39878  zrrnghm  39904
  Copyright terms: Public domain W3C validator