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

Theorem ralbiia 3168
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 272 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 3167 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wcel 2107  wral 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-ral 3147
This theorem is referenced by:  ralanid  3172  poinxp  5630  soinxp  5631  seinxp  5633  dffun8  6379  funcnv3  6420  fncnv  6423  fnres  6470  fvreseq0  6803  isoini2  7087  smores  7983  tfr3ALT  8032  resixp  8489  ixpfi2  8814  marypha1lem  8889  ac5num  9454  acni2  9464  acndom  9469  dfac4  9540  brdom7disj  9945  brdom6disj  9946  fpwwe2lem8  10051  axgroth6  10242  rabssnn0fi  13347  lo1res  14909  isprm5  16044  prmreclem2  16246  tsrss  17826  gass  18364  efgval2  18773  efgsres  18787  acsfn1p  19501  isdomn2  19994  islinds2  20876  isclo  21614  ptclsg  22142  ufilcmp  22559  cfilres  23817  ovolgelb  23999  volsup2  24124  vitali  24132  itg1climres  24233  itg2seq  24261  itg2monolem1  24269  itg2mono  24272  itg2i1fseq  24274  itg2cn  24282  ellimc2  24393  rolle  24505  lhop1  24529  itgsubstlem  24563  tdeglem4  24572  dvdsmulf1o  25688  dchrelbas2  25730  selbergsb  26068  axcontlem2  26668  dfconngr1  27884  hodsi  29469  ho01i  29522  ho02i  29523  lnopeqi  29702  nmcopexi  29721  nmcfnexi  29745  cnlnadjlem3  29763  cnlnadjlem5  29765  leop3  29819  pjssposi  29866  largei  29961  mdsl2i  30016  mdsl2bi  30017  elat2  30034  dmdbr5ati  30116  cdj3lem3b  30134  subfacp1lem3  32316  dfso3  32837  phpreu  34746  ptrecube  34762  mblfinlem1  34799  voliunnfl  34806  alephiso2  39785  ntrneiel2  40304  ismbl3  42140  ismbl4  42147  sge0lefimpt  42574  sbgoldbalt  43781
  Copyright terms: Public domain W3C validator