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

Theorem ralbiia 3166
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 262 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 3165 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wcel 2158  wral 3095
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897
This theorem depends on definitions:  df-bi 198  df-ral 3100
This theorem is referenced by:  poinxp  5381  soinxp  5382  seinxp  5384  dffun8  6126  funcnv3  6167  fncnv  6170  fnres  6215  fvreseq0  6536  isoini2  6810  smores  7682  tfr3ALT  7731  resixp  8177  ixpfi2  8500  marypha1lem  8575  ac5num  9139  acni2  9149  acndom  9154  dfac4  9225  brdom7disj  9635  brdom6disj  9636  fpwwe2lem8  9741  axgroth6  9932  rabssnn0fi  13005  lo1res  14509  isprm5  15632  prmreclem2  15834  tsrss  17424  gass  17931  efgval2  18334  efgsres  18348  isdomn2  19504  islinds2  20358  isclo  21101  ptclsg  21628  ufilcmp  22045  cfilres  23302  ovolgelb  23457  volsup2  23582  vitali  23590  itg1climres  23691  itg2seq  23719  itg2monolem1  23727  itg2mono  23730  itg2i1fseq  23732  itg2cn  23740  ellimc2  23851  rolle  23963  lhop1  23987  itgsubstlem  24021  tdeglem4  24030  dvdsmulf1o  25130  dchrelbas2  25172  selbergsb  25474  axcontlem2  26055  dfconngr1  27357  hodsi  28959  ho01i  29012  ho02i  29013  lnopeqi  29192  nmcopexi  29211  nmcfnexi  29235  cnlnadjlem3  29253  cnlnadjlem5  29255  leop3  29309  pjssposi  29356  largei  29451  mdsl2i  29506  mdsl2bi  29507  elat2  29524  dmdbr5ati  29606  cdj3lem3b  29624  subfacp1lem3  31484  dfso3  31920  phpreu  33703  ptrecube  33719  mblfinlem1  33756  voliunnfl  33763  acsfn1p  38267  ntrneiel2  38881  ismbl3  40679  ismbl4  40686  sge0lefimpt  41116  sbgoldbalt  42241
  Copyright terms: Public domain W3C validator