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

Theorem raleq 2896
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 2571 . 2  |-  F/_ x A
2 nfcv 2571 . 2  |-  F/_ x B
31, 2raleqf 2892 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652   A.wral 2697
This theorem is referenced by:  raleqi  2900  raleqdv  2902  raleqbi1dv  2904  sbralie  2937  r19.2zb  3710  inteq  4045  iineq1  4099  fri  4536  reusv6OLD  4726  reusv7OLD  4727  onminex  4779  tfinds  4831  frsn  4940  fncnv  5507  isoeq4  6034  f1oweALT  6066  frxp  6448  tfrlem1  6628  tfrlem3  6630  tfrlem12  6642  omeulem1  6817  ixpeq1  7065  undifixp  7090  ac6sfi  7343  frfi  7344  iunfi  7386  indexfi  7406  supeq1  7442  supeq2  7445  bnd2  7809  acneq  7916  aceq3lem  7993  dfac5lem4  7999  dfac8  8007  dfac9  8008  kmlem1  8022  kmlem10  8031  kmlem13  8034  cfval  8119  axcc2lem  8308  axcc4dom  8313  axdc3lem3  8324  axdc3lem4  8325  ac4c  8348  ac5  8349  ac6sg  8360  zorn2lem7  8374  xrsupsslem  10877  xrinfmsslem  10878  xrsupss  10879  xrinfmss  10880  rexanuz  12141  rexfiuz  12143  gcdcllem3  13005  isprs  14379  drsdirfi  14387  isdrs2  14388  ispos  14396  lubval  14428  glbval  14433  istos  14456  pospropd  14553  isdlat  14611  spwval2  14648  spwpr2  14652  mhmpropd  14736  isghm  14998  cntzval  15112  efgval  15341  iscmn  15411  dfrhm2  15813  lidldvgen  16318  ocvval  16886  isobs  16939  ist0  17376  cmpcovf  17446  is1stc  17496  2ndc1stc  17506  txflf  18030  ustuqtop4  18266  iscfilu  18310  ispsmet  18327  ismet  18345  isxmet  18346  cncfval  18910  lebnumlem3  18980  fmcfil  19217  iscfil3  19218  caucfil  19228  iscmet3  19238  cfilres  19241  minveclem3  19322  ovolfiniun  19389  finiunmbl  19430  volfiniun  19433  dvcn  19799  ulmval  20288  nb3grapr  21454  isplig  21757  isgrpo  21776  isablo  21863  isexid2  21905  ismndo2  21925  rngomndo  22001  ocval  22774  isofld  24227  ismbfm  24594  isanmbfm  24598  derangval  24845  setinds  25397  dfon2lem3  25404  dfon2lem7  25408  tfisg  25471  poseq  25520  wfrlem1  25530  wfrlem15  25544  frrlem1  25574  sltval2  25603  sltres  25611  nodense  25636  nobndup  25647  nobnddown  25648  nofulllem1  25649  dfrdg4  25787  tfrqfree  25788  mblfinlem  26234  mbfresfi  26243  isfne  26339  isref  26350  indexdom  26427  heibor1lem  26509  pridl  26638  smprngopr  26653  ispridlc  26671  setindtrs  27087  dford3lem2  27089  dfac11  27128  fnchoice  27667  stoweidlem31  27747  stoweidlem57  27773  bnj865  29231  bnj1154  29305  bnj1296  29327  bnj1463  29361
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702
  Copyright terms: Public domain W3C validator