ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  albii GIF version

Theorem albii 1404
Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)
Hypothesis
Ref Expression
albii.1 (𝜑𝜓)
Assertion
Ref Expression
albii (∀𝑥𝜑 ↔ ∀𝑥𝜓)

Proof of Theorem albii
StepHypRef Expression
1 albi 1402 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1385 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 103  wal 1287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  2albii  1405  hbxfrbi  1406  nfbii  1407  19.26-2  1416  19.26-3an  1417  alrot3  1419  alrot4  1420  albiim  1421  2albiim  1422  alnex  1433  nfalt  1515  aaanh  1523  aaan  1524  alinexa  1539  exintrbi  1569  19.21-2  1602  19.31r  1616  equsalh  1661  equsal  1662  sbcof2  1738  dvelimfALT2  1745  19.23vv  1812  sbanv  1817  pm11.53  1823  nfsbxy  1866  nfsbxyt  1867  sbcomxyyz  1894  sb9  1903  sbnf2  1905  2sb6  1908  sbcom2v  1909  sb6a  1912  2sb6rf  1914  sbalyz  1923  sbal  1924  sbal1yz  1925  sbal1  1926  sbalv  1929  2exsb  1933  nfsb4t  1938  dvelimf  1939  dveeq1  1943  sbal2  1946  sb8eu  1961  sb8euh  1971  eu1  1973  eu2  1992  mo3h  2001  moanim  2022  2eu4  2041  exists1  2044  eqcom  2090  hblem  2195  abeq2  2196  abeq1  2197  nfceqi  2224  abid2f  2253  dfrex2dc  2371  ralbii2  2388  r2alf  2395  nfraldya  2412  r3al  2420  r19.21t  2448  r19.23t  2479  rabid2  2543  rabbi  2544  ralv  2636  ceqsralt  2646  gencbval  2667  rspc2gv  2732  ralab  2773  ralrab2  2778  euind  2800  reu2  2801  reu3  2803  rmo4  2806  reu8  2809  rmo3f  2810  rmoim  2814  2reuswapdc  2817  reuind  2818  2rmorex  2819  ra5  2925  rmo2ilem  2926  rmo3  2928  dfss2  3012  ss2ab  3087  ss2rab  3095  rabss  3096  uniiunlem  3107  dfdif3  3108  ddifstab  3130  ssequn1  3168  unss  3172  ralunb  3179  ssin  3220  ssddif  3231  n0rf  3293  eq0  3299  eqv  3300  rabeq0  3310  abeq0  3311  disj  3328  disj3  3332  rgenm  3380  pwss  3440  ralsnsg  3475  ralsns  3476  disjsn  3499  euabsn2  3506  snss  3561  snsssn  3600  dfnfc2  3666  uni0b  3673  unissb  3678  elintrab  3695  ssintrab  3706  intun  3714  intpr  3715  dfiin2g  3758  iunss  3766  dfdisj2  3816  cbvdisj  3824  disjnim  3828  dftr2  3930  dftr5  3931  trint  3943  zfnuleu  3955  vnex  3962  inex1  3965  repizf2lem  3988  axpweq  3998  zfpow  4002  axpow2  4003  axpow3  4004  exmid01  4023  zfpair2  4028  ssextss  4038  frirrg  4168  sucel  4228  zfun  4252  uniex2  4254  setindel  4344  setind  4345  elirr  4347  en2lp  4360  zfregfr  4379  tfi  4387  peano5  4403  ssrel  4514  ssrel2  4516  eqrelrel  4527  reliun  4546  raliunxp  4565  relop  4574  dmopab3  4637  dm0rn0  4641  reldm0  4642  cotr  4800  issref  4801  asymref  4804  intirr  4805  sb8iota  4974  dffun2  5012  dffun4  5013  dffun6f  5015  dffun4f  5018  dffun7  5028  funopab  5035  funcnv2  5060  funcnv  5061  funcnveq  5063  fun2cnv  5064  fun11  5067  fununi  5068  funcnvuni  5069  funimaexglem  5083  fnres  5116  fnopabg  5123  rexrnmpt  5426  dff13  5529  oprabidlem  5662  eqoprab2b  5689  mpt22eqb  5736  ralrnmpt2  5741  dfer2  6273  ltexprlemdisj  7144  recexprlemdisj  7168  isprm2  11192  bj-nfalt  11322  bdceq  11390  bdcriota  11431  bj-axempty2  11442  bj-vprc  11444  bdinex1  11447  bj-zfpair2  11458  bj-uniex2  11464  bj-ssom  11488  bj-inf2vnlem2  11523  ss1oel2o  11545
  Copyright terms: Public domain W3C validator