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

Theorem ralbiia 3117
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 3116 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 2139  wral 3050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-ral 3055
This theorem is referenced by:  poinxp  5339  soinxp  5340  seinxp  5342  dffun8  6077  funcnv3  6120  fncnv  6123  fnres  6168  fvreseq0  6480  isoini2  6752  smores  7618  tfr3ALT  7667  resixp  8109  ixpfi2  8429  marypha1lem  8504  ac5num  9049  acni2  9059  acndom  9064  dfac4  9135  brdom7disj  9545  brdom6disj  9546  fpwwe2lem8  9651  axgroth6  9842  rabssnn0fi  12979  lo1res  14489  isprm5  15621  prmreclem2  15823  tsrss  17424  gass  17934  efgval2  18337  efgsres  18351  isdomn2  19501  islinds2  20354  isclo  21093  ptclsg  21620  ufilcmp  22037  cfilres  23294  ovolgelb  23448  volsup2  23573  vitali  23581  itg1climres  23680  itg2seq  23708  itg2monolem1  23716  itg2mono  23719  itg2i1fseq  23721  itg2cn  23729  ellimc2  23840  rolle  23952  lhop1  23976  itgsubstlem  24010  tdeglem4  24019  dvdsmulf1o  25119  dchrelbas2  25161  selbergsb  25463  axcontlem2  26044  dfconngr1  27340  hodsi  28943  ho01i  28996  ho02i  28997  lnopeqi  29176  nmcopexi  29195  nmcfnexi  29219  cnlnadjlem3  29237  cnlnadjlem5  29239  leop3  29293  pjssposi  29340  largei  29435  mdsl2i  29490  mdsl2bi  29491  elat2  29508  dmdbr5ati  29590  cdj3lem3b  29608  subfacp1lem3  31471  dfso3  31908  phpreu  33706  ptrecube  33722  mblfinlem1  33759  voliunnfl  33766  acsfn1p  38271  ntrneiel2  38886  ismbl3  40706  ismbl4  40713  sge0lefimpt  41143  sbgoldbalt  42179
  Copyright terms: Public domain W3C validator