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

Theorem albii 1402
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 1400 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1383 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff set class
Syntax hints:  wb 103  wal 1285
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 1379  ax-gen 1381
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  2albii  1403  hbxfrbi  1404  nfbii  1405  19.26-2  1414  19.26-3an  1415  alrot3  1417  alrot4  1418  albiim  1419  2albiim  1420  alnex  1431  nfalt  1513  aaanh  1521  aaan  1522  alinexa  1537  exintrbi  1567  19.21-2  1600  19.31r  1614  equsalh  1658  equsal  1659  sbcof2  1735  dvelimfALT2  1742  19.23vv  1809  sbanv  1814  pm11.53  1820  nfsbxy  1863  nfsbxyt  1864  sbcomxyyz  1891  sb9  1900  sbnf2  1902  2sb6  1905  sbcom2v  1906  sb6a  1909  2sb6rf  1911  sbalyz  1920  sbal  1921  sbal1yz  1922  sbal1  1923  sbalv  1926  2exsb  1930  nfsb4t  1935  dvelimf  1936  dveeq1  1940  sbal2  1943  sb8eu  1958  sb8euh  1968  eu1  1970  eu2  1989  mo3h  1998  moanim  2019  2eu4  2038  exists1  2041  eqcom  2087  hblem  2192  abeq2  2193  abeq1  2194  nfceqi  2221  abid2f  2249  dfrex2dc  2367  ralbii2  2384  r2alf  2391  nfraldya  2408  r3al  2416  r19.21t  2444  r19.23t  2475  rabid2  2538  rabbi  2539  ralv  2629  ceqsralt  2639  gencbval  2660  rspc2gv  2724  ralab  2765  ralrab2  2770  euind  2792  reu2  2793  reu3  2795  rmo4  2798  reu8  2801  rmoim  2804  2reuswapdc  2807  reuind  2808  2rmorex  2809  ra5  2915  rmo2ilem  2916  rmo3  2918  dfss2  3001  ss2ab  3075  ss2rab  3083  rabss  3084  uniiunlem  3095  dfdif3  3096  ddifstab  3118  ssequn1  3156  unss  3160  ralunb  3167  ssin  3208  ssddif  3219  n0rf  3281  eq0  3287  eqv  3288  rabeq0  3298  abeq0  3299  disj  3316  disj3  3320  rgenm  3368  pwss  3424  ralsnsg  3457  ralsns  3458  disjsn  3481  euabsn2  3488  snss  3543  snsssn  3582  dfnfc2  3648  uni0b  3655  unissb  3660  elintrab  3677  ssintrab  3688  intun  3696  intpr  3697  dfiin2g  3740  iunss  3748  dfdisj2  3797  cbvdisj  3805  dftr2  3906  dftr5  3907  trint  3919  zfnuleu  3931  vnex  3938  inex1  3941  repizf2lem  3964  axpweq  3974  zfpow  3978  axpow2  3979  axpow3  3980  exmid01  3999  zfpair2  4004  ssextss  4014  frirrg  4144  sucel  4204  zfun  4228  uniex2  4230  setindel  4320  setind  4321  elirr  4323  en2lp  4336  zfregfr  4355  tfi  4363  peano5  4379  ssrel  4487  ssrel2  4489  eqrelrel  4500  reliun  4519  raliunxp  4538  relop  4547  dmopab3  4610  dm0rn0  4614  reldm0  4615  cotr  4771  issref  4772  asymref  4775  intirr  4776  sb8iota  4944  dffun2  4982  dffun4  4983  dffun6f  4985  dffun4f  4988  dffun7  4998  funopab  5005  funcnv2  5030  funcnv  5031  funcnveq  5033  fun2cnv  5034  fun11  5037  fununi  5038  funcnvuni  5039  funimaexglem  5053  fnres  5086  fnopabg  5093  rexrnmpt  5390  dff13  5490  oprabidlem  5618  eqoprab2b  5645  mpt22eqb  5692  ralrnmpt2  5697  dfer2  6226  ltexprlemdisj  7086  recexprlemdisj  7110  isprm2  10893  bj-nfalt  11022  bdceq  11090  bdcriota  11131  bj-axempty2  11142  bj-vprc  11144  bdinex1  11147  bj-zfpair2  11158  bj-uniex2  11164  bj-ssom  11188  bj-inf2vnlem2  11223  ss1oel2o  11245
  Copyright terms: Public domain W3C validator