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

Theorem raleq 3358
 Description: Equality theorem for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) Remove usage of ax-10 2142, ax-11 2158, and ax-12 2175. (Revised by Steven Nguyen, 30-Apr-2023.)
Assertion
Ref Expression
raleq (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem raleq
StepHypRef Expression
1 biidd 265 . 2 (𝐴 = 𝐵 → (𝜑𝜑))
21raleqbi1dv 3356 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  ∀wral 3106 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870  df-ral 3111 This theorem is referenced by:  raleqi  3362  raleqdv  3364  sbralie  3418  r19.2zb  4399  inteq  4841  iineq1  4898  fri  5481  frsn  5603  fncnv  6397  isoeq4  7052  onminex  7502  tfinds  7554  f1oweALT  7655  frxp  7803  wfrlem1  7937  wfrlem15  7952  tfrlem1  7995  tfrlem12  8008  omeulem1  8191  ixpeq1  8455  undifixp  8481  ac6sfi  8746  frfi  8747  iunfi  8796  indexfi  8816  supeq1  8893  supeq2  8896  bnd2  9306  acneq  9454  aceq3lem  9531  dfac5lem4  9537  dfac8  9546  dfac9  9547  kmlem1  9561  kmlem10  9570  kmlem13  9573  cfval  9658  axcc2lem  9847  axcc4dom  9852  axdc3lem3  9863  axdc3lem4  9864  ac4c  9887  ac5  9888  ac6sg  9899  zorn2lem7  9913  xrsupsslem  12688  xrinfmsslem  12689  xrsupss  12690  xrinfmss  12691  fsuppmapnn0fiubex  13355  rexanuz  14697  rexfiuz  14699  modfsummod  15141  gcdcllem3  15840  lcmfval  15955  lcmf0val  15956  lcmfunsnlem  15975  coprmprod  15995  coprmproddvds  15997  isprs  17532  drsdirfi  17540  isdrs2  17541  ispos  17549  lubeldm  17583  lubval  17586  glbeldm  17596  glbval  17599  istos  17637  pospropd  17736  isdlat  17795  mhmpropd  17954  isghm  18350  cntzval  18443  efgval  18835  iscmn  18906  dfrhm2  19465  lidldvgen  20021  ocvval  20356  isobs  20409  coe1fzgsumd  20931  evl1gsumd  20981  mat0dimcrng  21075  mdetunilem9  21225  ist0  21925  cmpcovf  21996  is1stc  22046  2ndc1stc  22056  isref  22114  txflf  22611  ustuqtop4  22850  iscfilu  22894  ispsmet  22911  ismet  22930  isxmet  22931  cncfval  23493  lebnumlem3  23568  fmcfil  23876  iscfil3  23877  caucfil  23887  iscmet3  23897  cfilres  23900  minveclem3  24033  ovolfiniun  24105  finiunmbl  24148  volfiniun  24151  dvcn  24524  ulmval  24975  axtgcont1  26262  nb3grpr  27172  dfconngr1  27973  isconngr  27974  1conngr  27979  frgr0v  28047  isplig  28259  isgrpo  28280  isablo  28329  ocval  29063  acunirnmpt  30422  isomnd  30752  isorng  30923  prmidl  31023  ismbfm  31620  isanmbfm  31624  bnj865  32305  bnj1154  32381  bnj1296  32403  bnj1463  32437  derangval  32527  setinds  33136  dfon2lem3  33143  dfon2lem7  33147  tfisg  33168  poseq  33208  frrlem1  33236  frrlem13  33248  sltval2  33276  sltres  33282  nolesgn2o  33291  nodense  33309  nosupbnd2lem1  33328  brsslt  33367  dfrecs2  33524  dfrdg4  33525  isfne  33800  finixpnum  35042  mblfinlem1  35094  mbfresfi  35103  indexdom  35172  heibor1lem  35247  isexid2  35293  ismndo2  35312  rngomndo  35373  pridl  35475  smprngopr  35490  ispridlc  35508  setindtrs  39964  dford3lem2  39966  dfac11  40004  mnuop123d  40968  fnchoice  41656  axccdom  41851  axccd  41859  stoweidlem31  42671  stoweidlem57  42697  fourierdlem80  42826  fourierdlem103  42849  fourierdlem104  42850  isvonmbl  43275  paireqne  44026  requad2  44139  mgmhmpropd  44403  rnghmval  44513  zrrnghm  44539  bnd2d  45209
 Copyright terms: Public domain W3C validator