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

Theorem raleqbi1dv 3356
Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.) (Proof shortened by Steven Nguyen, 5-May-2023.)
Hypothesis
Ref Expression
raleqbi1dv.1 (𝐴 = 𝐵 → (𝜑𝜓))
Assertion
Ref Expression
raleqbi1dv (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑥)

Proof of Theorem raleqbi1dv
StepHypRef Expression
1 id 22 . 2 (𝐴 = 𝐵𝐴 = 𝐵)
2 raleqbi1dv.1 . 2 (𝐴 = 𝐵 → (𝜑𝜓))
31, 2raleqbidv 3354 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:  raleq  3358  isoeq4  7052  wfrlem1  7937  wfrlem4  7941  wfrlem15  7952  smo11  7984  dffi2  8871  inficl  8873  dffi3  8879  dfom3  9094  aceq1  9528  dfac5lem4  9537  kmlem1  9561  kmlem10  9570  kmlem13  9573  kmlem14  9574  cofsmo  9680  infpssrlem4  9717  axdc3lem2  9862  elwina  10097  elina  10098  iswun  10115  eltskg  10161  elgrug  10203  elnp  10398  elnpi  10399  dfnn2  11638  dfnn3  11639  dfuzi  12061  coprmprod  15995  coprmproddvds  15997  ismri  16894  isprs  17532  isdrs  17536  ispos  17549  istos  17637  pospropd  17736  isipodrs  17763  isdlat  17795  mhmpropd  17954  issubm  17960  subgacs  18305  nsgacs  18306  isghm  18350  ghmeql  18373  iscmn  18906  dfrhm2  19465  islss  19699  lssacs  19732  lmhmeql  19820  islbs  19841  lbsextlem1  19923  lbsextlem3  19925  lbsextlem4  19926  isobs  20409  mat0dimcrng  21075  istopg  21500  isbasisg  21552  basis2  21556  eltg2  21563  iscldtop  21700  neipeltop  21734  isreg  21937  regsep  21939  isnrm  21940  islly  22073  isnlly  22074  llyi  22079  nllyi  22080  islly2  22089  cldllycmp  22100  isfbas  22434  fbssfi  22442  isust  22809  elutop  22839  ustuqtop  22852  utopsnneip  22854  ispsmet  22911  ismet  22930  isxmet  22931  metrest  23131  cncfval  23493  fmcfil  23876  iscfil3  23877  caucfil  23887  iscmet3  23897  cfilres  23900  minveclem3  24033  wilthlem2  25654  wilthlem3  25655  wilth  25656  dfconngr1  27973  isconngr  27974  1conngr  27979  isplig  28259  isgrpo  28280  isablo  28329  disjabrex  30345  disjabrexf  30346  isomnd  30752  isorng  30923  isrnsiga  31482  isldsys  31525  isros  31537  issros  31544  bnj1286  32401  bnj1452  32434  kur14lem9  32574  cvmscbv  32618  cvmsi  32625  cvmsval  32626  frrlem1  33236  frrlem13  33248  neibastop1  33820  neibastop2lem  33821  neibastop2  33822  rdgssun  34795  isbnd  35218  ismndo2  35312  rngomndo  35373  isidl  35452  ispsubsp  37041  isnacs  39643  mzpclval  39664  elmzpcl  39665  mgmhmpropd  44403  issubmgm  44407  rnghmval  44513  zrrnghm  44539
  Copyright terms: Public domain W3C validator