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

Theorem ralbiia 3049
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)
Hypothesis
Ref Expression
ralbiia.1 (𝑥𝐴 → (𝜑𝜓))
Assertion
Ref Expression
ralbiia (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)

Proof of Theorem ralbiia
StepHypRef Expression
1 ralbiia.1 . . 3 (𝑥𝐴 → (𝜑𝜓))
21pm5.74i 260 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 3048 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2071  wral 2982
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818
This theorem depends on definitions:  df-bi 197  df-ral 2987
This theorem is referenced by:  poinxp  5259  soinxp  5260  seinxp  5262  dffun8  5997  funcnv3  6040  fncnv  6043  fnres  6088  fvreseq0  6400  isoini2  6672  smores  7537  tfr3ALT  7586  resixp  8028  ixpfi2  8348  marypha1lem  8423  ac5num  8940  acni2  8950  acndom  8955  dfac4  9026  brdom7disj  9434  brdom6disj  9435  fpwwe2lem8  9540  axgroth6  9731  rabssnn0fi  12868  lo1res  14378  isprm5  15510  prmreclem2  15712  tsrss  17313  gass  17823  efgval2  18226  efgsres  18240  isdomn2  19390  islinds2  20243  isclo  20982  ptclsg  21509  ufilcmp  21926  cfilres  23183  ovolgelb  23337  volsup2  23462  vitali  23470  itg1climres  23569  itg2seq  23597  itg2monolem1  23605  itg2mono  23608  itg2i1fseq  23610  itg2cn  23618  ellimc2  23729  rolle  23841  lhop1  23865  itgsubstlem  23899  tdeglem4  23908  dvdsmulf1o  25008  dchrelbas2  25050  selbergsb  25352  axcontlem2  25933  dfconngr1  27229  hodsi  28832  ho01i  28885  ho02i  28886  lnopeqi  29065  nmcopexi  29084  nmcfnexi  29108  cnlnadjlem3  29126  cnlnadjlem5  29128  leop3  29182  pjssposi  29229  largei  29324  mdsl2i  29379  mdsl2bi  29380  elat2  29397  dmdbr5ati  29479  cdj3lem3b  29497  subfacp1lem3  31360  dfso3  31797  phpreu  33593  ptrecube  33609  mblfinlem1  33646  voliunnfl  33653  acsfn1p  38156  ntrneiel2  38771  ismbl3  40591  ismbl4  40598  sge0lefimpt  41028  sbgoldbalt  42064
  Copyright terms: Public domain W3C validator