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

Theorem raleqbi1dv 3401
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 3399 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890  df-ral 3140
This theorem is referenced by:  raleq  3403  isoeq4  7062  wfrlem1  7943  wfrlem4  7947  wfrlem15  7958  smo11  7990  dffi2  8875  inficl  8877  dffi3  8883  dfom3  9098  aceq1  9531  dfac5lem4  9540  kmlem1  9564  kmlem10  9573  kmlem13  9576  kmlem14  9577  cofsmo  9679  infpssrlem4  9716  axdc3lem2  9861  elwina  10096  elina  10097  iswun  10114  eltskg  10160  elgrug  10202  elnp  10397  elnpi  10398  dfnn2  11639  dfnn3  11640  dfuzi  12061  coprmprod  15993  coprmproddvds  15995  ismri  16890  isprs  17528  isdrs  17532  ispos  17545  istos  17633  pospropd  17732  isipodrs  17759  isdlat  17791  mhmpropd  17950  issubm  17956  subgacs  18251  nsgacs  18252  isghm  18296  ghmeql  18319  iscmn  18843  dfrhm2  19398  islss  19635  lssacs  19668  lmhmeql  19756  islbs  19777  lbsextlem1  19859  lbsextlem3  19861  lbsextlem4  19862  isobs  20792  mat0dimcrng  21007  istopg  21431  isbasisg  21483  basis2  21487  eltg2  21494  iscldtop  21631  neipeltop  21665  isreg  21868  regsep  21870  isnrm  21871  islly  22004  isnlly  22005  llyi  22010  nllyi  22011  islly2  22020  cldllycmp  22031  isfbas  22365  fbssfi  22373  isust  22739  elutop  22769  ustuqtop  22782  utopsnneip  22784  ispsmet  22841  ismet  22860  isxmet  22861  metrest  23061  cncfval  23423  fmcfil  23802  iscfil3  23803  caucfil  23813  iscmet3  23823  cfilres  23826  minveclem3  23959  wilthlem2  25573  wilthlem3  25574  wilth  25575  dfconngr1  27894  isconngr  27895  1conngr  27900  isplig  28180  isgrpo  28201  isablo  28250  disjabrex  30260  disjabrexf  30261  isomnd  30629  isorng  30799  isrnsiga  31271  isldsys  31314  isros  31326  issros  31333  bnj1286  32188  bnj1452  32221  kur14lem9  32358  cvmscbv  32402  cvmsi  32409  cvmsval  32410  frrlem1  33020  frrlem13  33032  neibastop1  33604  neibastop2lem  33605  neibastop2  33606  rdgssun  34541  isbnd  34939  ismndo2  35033  rngomndo  35094  isidl  35173  ispsubsp  36761  isnacs  39179  mzpclval  39200  elmzpcl  39201  mgmhmpropd  43929  issubmgm  43933  rnghmval  44090  zrrnghm  44116
  Copyright terms: Public domain W3C validator