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

Theorem ralbiia 3091
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 271 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 3089 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wcel 2104  wral 3062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 206  df-ral 3063
This theorem is referenced by:  ralbii  3093  ralanid  3095  poinxp  5678  soinxp  5679  seinxp  5681  dffun8  6491  funcnv3  6533  fncnv  6536  fnres  6590  fvreseq0  6947  isoini2  7242  smores  8214  tfr3ALT  8264  resixp  8752  ixpfi2  9165  marypha1lem  9240  ac5num  9842  acni2  9852  acndom  9857  dfac4  9928  brdom7disj  10337  brdom6disj  10338  fpwwe2lem7  10443  axgroth6  10634  rabssnn0fi  13756  lo1res  15317  isprm5  16461  prmreclem2  16667  tsrss  18356  gass  18956  efgval2  19379  efgsres  19393  acsfn1p  20116  isdomn2  20619  islinds2  21069  isclo  22287  ptclsg  22815  ufilcmp  23232  cfilres  24509  ovolgelb  24693  volsup2  24818  vitali  24826  itg1climres  24928  itg2seq  24956  itg2monolem1  24964  itg2mono  24967  itg2i1fseq  24969  itg2cn  24977  ellimc2  25090  rolle  25203  lhop1  25227  itgsubstlem  25261  tdeglem4  25273  tdeglem4OLD  25274  dvdsmulf1o  26392  dchrelbas2  26434  selbergsb  26772  axcontlem2  27382  dfconngr1  28601  hodsi  30186  ho01i  30239  ho02i  30240  lnopeqi  30419  nmcopexi  30438  nmcfnexi  30462  cnlnadjlem3  30480  cnlnadjlem5  30482  leop3  30536  pjssposi  30583  largei  30678  mdsl2i  30733  mdsl2bi  30734  elat2  30751  dmdbr5ati  30833  cdj3lem3b  30851  subfacp1lem3  33193  dfso3  33713  phpreu  35809  ptrecube  35825  mblfinlem1  35862  voliunnfl  35869  disjressuc2  36602  alephiso2  41378  ntrneiel2  41909  ismbl3  43756  ismbl4  43763  sge0lefimpt  44191  sbgoldbalt  45477
  Copyright terms: Public domain W3C validator