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

Theorem raleq 3285
Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Assertion
Ref Expression
raleq (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq
StepHypRef Expression
1 nfcv 2911 . 2 𝑥𝐴
2 nfcv 2911 . 2 𝑥𝐵
31, 2raleqf 3281 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1629  wral 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2152  ax-10 2172  ax-11 2188  ax-12 2201  ax-ext 2749
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1632  df-ex 1851  df-nf 1856  df-cleq 2762  df-clel 2765  df-nfc 2900  df-ral 3064
This theorem is referenced by:  raleqi  3289  raleqdv  3291  raleqbi1dv  3293  sbralie  3331  r19.2zb  4199  inteq  4611  iineq1  4666  fri  5210  frsn  5328  fncnv  6101  isoeq4  6711  onminex  7152  tfinds  7204  f1oweALT  7297  frxp  7436  wfrlem1  7564  wfrlem15  7580  tfrlem1  7623  tfrlem12  7636  omeulem1  7814  ixpeq1  8071  undifixp  8096  ac6sfi  8358  frfi  8359  iunfi  8408  indexfi  8428  supeq1  8505  supeq2  8508  bnd2  8918  acneq  9064  aceq3lem  9141  dfac5lem4  9147  dfac8  9157  dfac9  9158  kmlem1  9172  kmlem10  9181  kmlem13  9184  cfval  9269  axcc2lem  9458  axcc4dom  9463  axdc3lem3  9474  axdc3lem4  9475  ac4c  9498  ac5  9499  ac6sg  9510  zorn2lem7  9524  xrsupsslem  12341  xrinfmsslem  12342  xrsupss  12343  xrinfmss  12344  fsuppmapnn0fiubex  12999  rexanuz  14296  rexfiuz  14298  modfsummod  14737  gcdcllem3  15437  lcmfval  15548  lcmf0val  15549  lcmfunsnlem  15568  coprmprod  15588  coprmproddvds  15590  isprs  17144  drsdirfi  17152  isdrs2  17153  ispos  17161  lubeldm  17195  lubval  17198  glbeldm  17208  glbval  17211  istos  17249  pospropd  17348  isdlat  17407  mhmpropd  17555  isghm  17874  cntzval  17967  efgval  18343  iscmn  18413  dfrhm2  18933  lidldvgen  19476  coe1fzgsumd  19893  evl1gsumd  19942  ocvval  20234  isobs  20287  mat0dimcrng  20500  mdetunilem9  20650  ist0  21351  cmpcovf  21421  is1stc  21471  2ndc1stc  21481  isref  21539  txflf  22036  ustuqtop4  22274  iscfilu  22318  ispsmet  22335  ismet  22354  isxmet  22355  cncfval  22917  lebnumlem3  22988  fmcfil  23295  iscfil3  23296  caucfil  23306  iscmet3  23316  cfilres  23319  minveclem3  23425  ovolfiniun  23495  finiunmbl  23538  volfiniun  23541  dvcn  23910  ulmval  24360  axtgcont1  25594  tgcgr4  25653  nb3grpr  26513  prcliscplgr  26550  dfconngr1  27372  isconngr  27373  1conngr  27378  frgr0v  27447  isplig  27671  isgrpo  27692  isablo  27741  ocval  28480  acunirnmpt  29800  isomnd  30042  isorng  30140  ismbfm  30655  isanmbfm  30659  bnj865  31332  bnj1154  31406  bnj1296  31428  bnj1463  31462  derangval  31488  setinds  32020  dfon2lem3  32027  dfon2lem7  32031  tfisg  32053  poseq  32091  frrlem1  32118  sltval2  32147  sltres  32153  nolesgn2o  32162  nodense  32180  nosupbnd2lem1  32199  brsslt  32238  dfrecs2  32395  dfrdg4  32396  isfne  32672  finixpnum  33727  mblfinlem1  33779  mbfresfi  33788  indexdom  33861  heibor1lem  33940  isexid2  33986  ismndo2  34005  rngomndo  34066  pridl  34168  smprngopr  34183  ispridlc  34201  setindtrs  38118  dford3lem2  38120  dfac11  38158  fnchoice  39711  axccdom  39935  axccd  39948  stoweidlem31  40766  stoweidlem57  40792  fourierdlem80  40921  fourierdlem103  40944  fourierdlem104  40945  isvonmbl  41373  mgmhmpropd  42310  rnghmval  42416  zrrnghm  42442  bnd2d  42953
  Copyright terms: Public domain W3C validator