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

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

Proof of Theorem raleqbi1dv
StepHypRef Expression
1 raleq 3168 . 2 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜑))
2 raleqd.1 . . 3 (𝐴 = 𝐵 → (𝜑𝜓))
32ralbidv 3015 . 2 (𝐴 = 𝐵 → (∀𝑥𝐵 𝜑 ↔ ∀𝑥𝐵 𝜓))
41, 3bitrd 268 1 (𝐴 = 𝐵 → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐵 𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946
This theorem is referenced by:  isoeq4  6610  wfrlem1  7459  wfrlem4  7463  wfrlem15  7474  smo11  7506  dffi2  8370  inficl  8372  dffi3  8378  dfom3  8582  aceq1  8978  dfac5lem4  8987  kmlem1  9010  kmlem10  9019  kmlem13  9022  kmlem14  9023  cofsmo  9129  infpssrlem4  9166  axdc3lem2  9311  elwina  9546  elina  9547  iswun  9564  eltskg  9610  elgrug  9652  elnp  9847  elnpi  9848  dfnn2  11071  dfnn3  11072  dfuzi  11506  coprmprod  15422  coprmproddvds  15424  ismri  16338  isprs  16977  isdrs  16981  ispos  16994  istos  17082  pospropd  17181  isipodrs  17208  isdlat  17240  mhmpropd  17388  issubm  17394  subgacs  17676  nsgacs  17677  isghm  17707  ghmeql  17730  iscmn  18246  dfrhm2  18765  islss  18983  lssacs  19015  lmhmeql  19103  islbs  19124  lbsextlem1  19206  lbsextlem3  19208  lbsextlem4  19209  isobs  20112  mat0dimcrng  20324  istopg  20748  isbasisg  20799  basis2  20803  eltg2  20810  iscldtop  20947  neipeltop  20981  isreg  21184  regsep  21186  isnrm  21187  islly  21319  isnlly  21320  llyi  21325  nllyi  21326  islly2  21335  cldllycmp  21346  isfbas  21680  fbssfi  21688  isust  22054  elutop  22084  ustuqtop  22097  utopsnneip  22099  ispsmet  22156  ismet  22175  isxmet  22176  metrest  22376  cncfval  22738  fmcfil  23116  iscfil3  23117  caucfil  23127  iscmet3  23137  cfilres  23140  minveclem3  23246  wilthlem2  24840  wilthlem3  24841  wilth  24842  dfconngr1  27166  isconngr  27167  isplig  27458  isgrpo  27479  isablo  27528  disjabrex  29521  disjabrexf  29522  isomnd  29829  isorng  29927  isrnsigaOLD  30303  isrnsiga  30304  isldsys  30347  isros  30359  issros  30366  bnj1286  31213  bnj1452  31246  kur14lem9  31322  cvmscbv  31366  cvmsi  31373  cvmsval  31374  frrlem1  31905  neibastop1  32479  neibastop2lem  32480  neibastop2  32481  isbnd  33709  ismndo2  33803  rngomndo  33864  isidl  33943  ispsubsp  35349  isnacs  37584  mzpclval  37605  elmzpcl  37606  mgmhmpropd  42110  issubmgm  42114  rnghmval  42216  zrrnghm  42242
  Copyright terms: Public domain W3C validator