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

Theorem ralbiia 2978
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 2977 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wcel 1992  wral 2912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ral 2917
This theorem is referenced by:  poinxp  5148  soinxp  5149  seinxp  5151  dffun8  5877  funcnv3  5919  fncnv  5922  fnres  5967  fvreseq0  6274  isoini2  6544  smores  7395  tfr3ALT  7444  resixp  7888  ixpfi2  8209  marypha1lem  8284  ac5num  8804  acni2  8814  acndom  8819  dfac4  8890  brdom7disj  9298  brdom6disj  9299  fpwwe2lem8  9404  axgroth6  9595  rabssnn0fi  12722  lo1res  14219  isprm5  15338  prmreclem2  15540  tsrss  17139  gass  17650  efgval2  18053  efgsres  18067  isdomn2  19213  islinds2  20066  isclo  20796  ptclsg  21323  ufilcmp  21741  cfilres  22997  ovolgelb  23150  volsup2  23274  vitali  23283  itg1climres  23382  itg2seq  23410  itg2monolem1  23418  itg2mono  23421  itg2i1fseq  23423  itg2cn  23431  ellimc2  23542  rolle  23652  lhop1  23676  itgsubstlem  23710  tdeglem4  23719  dvdsmulf1o  24815  dchrelbas2  24857  selbergsb  25159  axcontlem2  25740  dfconngr1  26908  hodsi  28474  ho01i  28527  ho02i  28528  lnopeqi  28707  nmcopexi  28726  nmcfnexi  28750  cnlnadjlem3  28768  cnlnadjlem5  28770  leop3  28824  pjssposi  28871  largei  28966  mdsl2i  29021  mdsl2bi  29022  elat2  29039  dmdbr5ati  29121  cdj3lem3b  29139  subfacp1lem3  30864  dfso3  31302  phpreu  33011  ptrecube  33027  mblfinlem1  33064  voliunnfl  33071  acsfn1p  37236  ntrneiel2  37852  ismbl3  39497  ismbl4  39504  sge0lefimpt  39934  sgoldbalt  40952
  Copyright terms: Public domain W3C validator