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

Theorem albii 1811
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 1810 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1789 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wal 1526
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208
This theorem is referenced by:  2albii  1812  hbxfrbi  1816  alex  1817  2nalexn  1819  2exnaln  1820  imnang  1833  alexn  1836  nfnbi  1846  19.26-2  1863  19.26-3an  1864  19.43OLD  1875  albiim  1881  2albiim  1882  empty  1898  19.32v  1932  19.31v  1933  19.23vv  1935  pm11.53v  1936  19.12vvv  1986  equsalvw  2001  2sb6  2085  sbrimvlem  2092  sbcom3vv  2097  alrot3  2154  alrot4  2155  sbal  2156  sbalv  2157  19.21-2  2199  19.32  2225  19.31  2226  equsalv  2258  sbn  2278  aaan  2344  pm11.53  2358  19.12vv  2359  equsal  2430  2sb6rf  2489  2sb6rfOLD  2490  sbcom3  2541  sb8eulem  2677  eu1  2687  2mo2  2725  2eu1  2728  2eu1OLD  2729  2eu1v  2730  2eu3  2732  2eu3OLD  2733  euae  2740  nulmo  2795  hblem  2940  hblemg  2941  abeq2  2942  abeq1  2943  abbiOLD  2952  nfcrii  2967  nfceqi  2970  abeq2f  3010  abeq2fOLD  3011  ralbii2  3160  ralanidOLD  3166  r19.21v  3172  r2allem  3197  r3al  3199  r19.21t  3211  ralcom4  3232  r19.23t  3310  rabid2  3379  rabid2f  3380  rabbi  3381  eqv  3500  eqvf  3501  abv  3502  ralv  3517  ceqsralt  3526  rspc2gv  3629  ralxpxfr2d  3636  ralab  3681  ralrab2  3687  euind  3712  reu2  3713  reu3  3715  rmo4  3718  reu8  3721  rmo3f  3722  rmoim  3728  2reuswap  3734  2reuswap2  3735  reuind  3741  2reu5lem2  3744  2reu5lem3  3745  2rmoswap  3749  rmo2  3867  rmo3  3869  rmo3OLD  3870  rmoanim  3875  dfss2  3952  ss2ab  4036  ss2rab  4044  rabss  4045  uniiunlem  4058  dfdif3  4088  ssequn1  4153  unss  4157  ralunb  4164  ssin  4204  eq0f  4302  ssdif0  4320  inssdif0  4326  ab0  4330  disj  4395  disj3  4399  ssundif  4429  ralf0  4453  pwss  4555  rabsssn  4597  ralsnsg  4598  disjsn  4639  snssg  4709  pwpw0  4738  pwsnALT  4823  dfnfc2  4848  unissb  4861  elintrab  4879  ssintrab  4890  intun  4899  intpr  4900  dfiin2g  4948  iunss  4960  dfdisj2  5024  cbvdisj  5032  disjor  5037  dftr2  5165  dftr5  5166  axrep1  5182  axrep5  5187  axrep6  5188  axsepgfromrep  5192  axnulALT  5199  vnex  5209  inex1  5212  axpweq  5256  zfpow  5258  axpow2  5259  axpow3  5260  nfnid  5267  dtruALT  5279  reusv2lem4  5292  zfpair2  5321  dtruALT2  5326  ssextss  5337  moabex  5342  dffr2  5513  dfepfr  5533  frinxp  5627  ssrel2  5652  eqrelrel  5663  reliun  5682  raliunxp  5703  relop  5714  dmopab3  5781  dm0rn0  5788  reldm0  5791  iresn0n0  5916  dffr3  5955  cotrg  5964  idrefALT  5966  asymref  5969  asymref2  5970  intirr  5971  dffr4  6157  sucel  6257  sb8iota  6318  dffun2  6358  dffun3  6359  dffun4  6360  dffun5  6361  dffun6f  6362  dffun7  6375  funopab  6383  funcnv2  6415  funcnv  6416  fun2cnv  6418  fun11  6421  fununi  6422  fnres  6467  mptfnf  6476  fnopabg  6478  brprcneu  6655  dffv2  6749  fvn0ssdmfun  6834  dff13  7004  eqoprab2bw  7213  eqoprab2b  7214  mpo2eqb  7272  ralrnmpo  7278  zfun  7451  uniex2  7453  funcnvuni  7625  dfer2  8279  fiint  8783  marypha1lem  8885  marypha2lem3  8889  inf2  9074  axinf2  9091  scottexs  9304  scott0s  9305  aceq1  9531  dfac4  9536  dfac7  9546  dfac0  9547  dfac1  9548  dfac10  9551  dfac10c  9552  dfac10b  9553  kmlem4  9567  kmlem12  9575  kmlem14  9577  kmlem15  9578  kmlem16  9579  dfackm  9580  ac6n  9895  axpowndlem3  10009  zfcndrep  10024  zfcndun  10025  zfcndpow  10026  axgroth5  10234  axgroth2  10235  axgroth4  10242  grothprim  10244  sstskm  10252  fimaxre3  11575  infm3  11588  nnwos  12303  cotr2g  14324  brtrclfv  14350  trclfvcotr  14357  rpnnen2lem12  15566  isprm2  16014  vdwmc2  16303  pgpfac1  19131  pgpfac  19135  iunocv  20753  2ndcdisj2  21993  hausdiag  22181  rnelfmlem  22488  alexsubALTlem3  22585  cnextfun  22600  itg2leub  24262  mptelee  26608  nmoubi  28476  nmobndseqi  28483  nmobndseqiALT  28484  isch2  28927  isch3  28945  choc0  29030  nmopub  29612  nmfnleub  29629  xfree2  30149  nelbOLD  30159  moel  30179  mo5f  30180  nmo  30181  reuxfrdf  30182  rabeqsnd  30191  inpr0  30219  cbvdisjf  30249  disjorf  30257  ssrelf  30294  funcnvmpt  30340  funcnv5mpt  30341  ballotlem2  31645  bnj89  31890  bnj115  31894  bnj1143  31961  bnj110  32029  bnj611  32089  bnj864  32093  bnj865  32094  bnj1000  32112  bnj978  32120  bnj1049  32143  bnj1052  32144  bnj1090  32148  bnj1030  32156  bnj1133  32158  bnj1171  32169  bnj1172  32170  bnj1174  32172  bnj1176  32174  bnj1204  32181  bnj1253  32186  bnj1388  32202  bnj1523  32240  axrepprim  32825  axunprim  32826  axpowprim  32827  axinfprim  32829  axacprim  32830  untuni  32832  dffr5  32886  elintfv  32904  dfon2lem8  32932  dfon2lem9  32933  19.12b  32943  brtxpsd3  33254  dfom5b  33270  dffun10  33272  bj-notalbii  33845  bj-ssbeq  33883  bj-ax12ssb  33888  bj-hbext  33941  bj-nfalt  33942  bj-nnfalt  33992  bj-nnfext  33993  ax11-pm2  34056  bj-sbnf  34061  bj-sblem  34065  bj-ralvw  34092  bj-sbeq  34115  bj-nfcf  34139  bj-snsetex  34172  bj-rcleqf  34234  fvineqsneq  34575  wl-equsalvw  34659  wl-equsalcom  34663  wl-sb8et  34670  wl-2sb6d  34675  wl-alanbii  34686  wl-sb8eut  34694  wl-dfralsb  34718  wl-dfralflem  34719  wl-dfralv  34722  wl-dfrexex  34731  wl-dfrexsb  34732  wl-dfrmosb  34734  wl-dfrmov  34735  poimirlem25  34798  poimirlem30  34803  heibor1lem  34968  sbcalfi  35275  mpobi123f  35321  mptbi12f  35325  3albii  35390  ineccnvmo  35492  alrmomorn  35493  cocossss  35561  cossssid3  35589  cossssid4  35590  cosscnvssid4  35597  trcoss2  35604  dfeldisj4  35833  dfeldisj5  35834  dvelimf-o  35945  axc11n-16  35954  pmapglbx  36785  sn-axrep5v  38986  dford4  39504  rp-fakeinunass  39759  rababg  39811  elmapintrab  39814  elinintrab  39815  undmrnresiss  39842  clss2lem  39849  cotrintab  39852  elintima  39876  ss2iundf  39882  relexp0eq  39924  dfhe3  39999  snhesn  40010  psshepw  40012  dffrege76  40163  frege77  40164  frege110  40197  dffrege115  40202  frege116  40203  frege118  40205  frege131  40218  ntrneikb  40322  ismnuprim  40507  rr-grothprimbi  40508  pm10.541  40576  pm10.542  40577  19.21vv  40585  19.31vv  40593  19.28vv  40595  pm11.62  40603  axc11next  40615  pm13.196a  40623  2sbc6g  40624  elnev  40647  hbexgVD  41117  iunssf  41229  rabssf  41262  2rexsb  43176  dfich2  43490  dfich2ai  43491  ichal  43504  spr0nelg  43515  dffun3f  44713  setrec1lem2  44719  setrec2  44726  setis  44728  alimp-surprise  44809  alimp-no-surprise  44810
  Copyright terms: Public domain W3C validator