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

Theorem raleq 2907
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 2569 . 2  |-  F/_ x A
2 nfcv 2569 . 2  |-  F/_ x B
31, 2raleqf 2903 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 1362   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ral 2710
This theorem is referenced by:  raleqi  2911  raleqdv  2913  raleqbi1dv  2915  sbralie  2950  r19.2zb  3758  inteq  4119  iineq1  4173  reusv6OLD  4491  reusv7OLD  4492  fri  4669  frsn  4896  fncnv  5470  isoeq4  6000  onminex  6407  tfinds  6459  f1oweALT  6550  frxp  6671  tfrlem1  6821  tfrlem12  6834  omeulem1  7009  ixpeq1  7262  undifixp  7287  ac6sfi  7544  frfi  7545  iunfi  7587  indexfi  7607  supeq1  7683  supeq2  7686  bnd2  8088  acneq  8201  aceq3lem  8278  dfac5lem4  8284  dfac8  8292  dfac9  8293  kmlem1  8307  kmlem10  8316  kmlem13  8319  cfval  8404  axcc2lem  8593  axcc4dom  8598  axdc3lem3  8609  axdc3lem4  8610  ac4c  8633  ac5  8634  ac6sg  8645  zorn2lem7  8659  xrsupsslem  11256  xrinfmsslem  11257  xrsupss  11258  xrinfmss  11259  rexanuz  12816  rexfiuz  12818  gcdcllem3  13679  isprs  15082  drsdirfi  15090  isdrs2  15091  ispos  15099  lubeldm  15133  lubval  15136  glbeldm  15146  glbval  15149  istos  15187  pospropd  15286  isdlat  15345  mhmpropd  15452  isghm  15726  cntzval  15818  efgval  16193  iscmn  16263  dfrhm2  16741  lidldvgen  17258  ocvval  17933  isobs  17986  mdetunilem9  18267  ist0  18765  cmpcovf  18835  is1stc  18886  2ndc1stc  18896  txflf  19420  ustuqtop4  19660  iscfilu  19704  ispsmet  19721  ismet  19739  isxmet  19740  cncfval  20305  lebnumlem3  20376  fmcfil  20624  iscfil3  20625  caucfil  20635  iscmet3  20645  cfilres  20648  minveclem3  20757  ovolfiniun  20825  finiunmbl  20866  volfiniun  20869  dvcn  21236  ulmval  21729  axtgcont1  22813  nb3grapr  23183  isplig  23486  isgrpo  23505  isablo  23592  isexid2  23634  ismndo2  23654  rngomndo  23730  ocval  24505  isomnd  25987  isorng  26119  ismbfm  26520  isanmbfm  26524  derangval  26902  setinds  27437  dfon2lem3  27444  dfon2lem7  27448  tfisg  27511  poseq  27560  wfrlem1  27570  wfrlem15  27584  frrlem1  27614  sltval2  27643  sltres  27651  nodense  27676  nobndup  27687  nobnddown  27688  nofulllem1  27689  dfrdg4  27827  tfrqfree  27828  finixpnum  28255  mblfinlem1  28269  mbfresfi  28279  isfne  28381  isref  28392  indexdom  28469  heibor1lem  28549  pridl  28678  smprngopr  28693  ispridlc  28711  setindtrs  29216  dford3lem2  29218  dfac11  29257  fnchoice  29593  stoweidlem31  29669  stoweidlem57  29695  modfsummod  30088  rusgrasn  30400  mat0dimcrng  30643  bnj865  31615  bnj1154  31689  bnj1296  31711  bnj1463  31745
  Copyright terms: Public domain W3C validator