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

Theorem raleq 2736
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 2419 . 2  |-  F/_ x A
2 nfcv 2419 . 2  |-  F/_ x B
31, 2raleqf 2732 1  |-  ( A  =  B  ->  ( A. x  e.  A  ph  <->  A. x  e.  B  ph ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623   A.wral 2543
This theorem is referenced by:  raleqi  2740  raleqdv  2742  raleqbi1dv  2744  sbralie  2777  r19.2zb  3544  inteq  3865  iineq1  3919  fri  4355  reusv6OLD  4545  reusv7OLD  4546  onminex  4598  tfinds  4650  frsn  4760  fncnv  5314  isoeq4  5819  f1oweALT  5851  frxp  6225  tfrlem1  6391  tfrlem3  6393  tfrlem12  6405  omeulem1  6580  ixpeq1  6827  undifixp  6852  ac6sfi  7101  frfi  7102  iunfi  7144  indexfi  7163  supeq1  7198  supeq2  7201  bnd2  7563  acneq  7670  aceq3lem  7747  dfac5lem4  7753  dfac8  7761  dfac9  7762  kmlem1  7776  kmlem10  7785  kmlem13  7788  cfval  7873  axcc2lem  8062  axcc4dom  8067  axdc3lem3  8078  axdc3lem4  8079  ac4c  8103  ac5  8104  ac6sg  8115  zorn2lem7  8129  xrsupsslem  10625  xrinfmsslem  10626  xrsupss  10627  xrinfmss  10628  rexanuz  11829  rexfiuz  11831  gcdcllem3  12692  isprs  14064  drsdirfi  14072  isdrs2  14073  ispos  14081  lubval  14113  glbval  14118  istos  14141  pospropd  14238  isdlat  14296  spwval2  14333  spwpr2  14337  mhmpropd  14421  isghm  14683  cntzval  14797  efgval  15026  iscmn  15096  dfrhm2  15498  lidldvgen  16007  ocvval  16567  isobs  16620  ist0  17048  cmpcovf  17118  is1stc  17167  2ndc1stc  17177  txflf  17701  ismet  17888  isxmet  17889  cncfval  18392  lebnumlem3  18461  fmcfil  18698  iscfil3  18699  caucfil  18709  iscmet3  18719  cfilres  18722  minveclem3  18793  ovolfiniun  18860  finiunmbl  18901  volfiniun  18904  dvcn  19270  ulmval  19759  isplig  20844  isgrpo  20863  isablo  20950  isexid2  20992  ismndo2  21012  rngomndo  21088  ocval  21859  prsiga  23492  ismbfm  23557  isanmbfm  23561  derangval  23698  setinds  24134  dfon2lem3  24141  dfon2lem7  24145  tfisg  24204  poseq  24253  wfrlem1  24256  wfrlem15  24270  frrlem1  24281  sltval2  24310  sltres  24318  nodense  24343  nobndup  24354  nobnddown  24355  nofulllem1  24356  dfrdg4  24488  tfrqfree  24489  bpolyval  24784  hfext  24813  ac5g  25075  prjmapcp2  25170  islatalg  25183  ubos  25256  defse3  25272  ablocomgrp  25342  com2i  25416  ununr  25420  lvsovso  25626  tcnvec  25690  isibg2  26110  isfne  26268  isref  26279  indexdom  26413  heibor1lem  26533  pridl  26662  smprngopr  26677  ispridlc  26695  setindtrs  27118  dford3lem2  27120  dfac11  27160  fnchoice  27700  stoweidlem31  27780  stoweidlem57  27806  bnj865  28955  bnj1154  29029  bnj1296  29051  bnj1463  29085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548
  Copyright terms: Public domain W3C validator