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

Theorem albii 1744
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 1743 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1721 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1478
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
This theorem is referenced by:  2albii  1745  hbxfrbi  1749  alex  1750  2nalexn  1752  2exnaln  1753  imnang  1766  alexn  1768  nfnbi  1778  19.26-2  1796  19.26-3an  1797  19.43OLD  1808  albiim  1813  2albiim  1814  nfbiiOLD  1833  19.32v  1866  19.31v  1867  19.23vv  1900  pm11.53v  1903  19.12vvv  1904  equsalvw  1928  alrot3  2035  alrot4  2036  19.21-2  2076  19.23t  2077  19.32  2099  19.31  2100  equsalhw  2120  aaan  2167  pm11.53  2178  19.12vv  2179  19.21-2OLD  2214  19.23tOLD  2217  equsal  2290  sbcom3  2410  2sb6  2443  2sb6rf  2451  sbex  2462  sbalv  2463  sb8eu  2502  eu1  2509  2mo2  2549  2eu1  2552  2eu3  2554  exists1  2560  hblem  2728  abeq2  2729  abeq1  2730  abbi  2734  abeq2f  2788  r2allem  2933  r3al  2936  r19.21t  2951  r19.21v  2956  ralbii2  2974  r19.23t  3016  rabid2  3111  rabid2f  3112  rabbi  3113  eqvf  3194  abv  3196  ralv  3209  ceqsralt  3219  rspc2gv  3310  ralxpxfr2d  3316  ralab  3354  ralrab2  3359  euind  3380  reu2  3381  reu3  3383  rmo4  3386  reu8  3389  rmoim  3394  2reuswap  3397  reuind  3398  2reu5lem2  3401  2reu5lem3  3402  rmo2  3512  rmo3  3514  dfss2  3577  ss2ab  3655  ss2rab  3663  rabss  3664  uniiunlem  3675  ssequn1  3767  unss  3771  ralunb  3778  ssin  3819  eq0f  3907  n0fOLD  3910  ssdif0  3922  inssdif0  3927  ab0  3931  disj  3995  disj3  3999  ssundif  4030  ralf0  4056  pwss  4153  rabsssn  4193  ralsnsg  4194  disjsn  4223  euabsn2  4237  snss  4293  pwpw0  4319  pwsnALT  4404  dfnfc2  4427  dfnfc2OLD  4428  unissb  4442  elintrab  4460  ssintrab  4472  intun  4481  intpr  4482  dfiin2g  4526  iunss  4534  dfdisj2  4595  cbvdisj  4603  disjor  4607  dftr2  4724  dftr5  4725  trint  4738  axrep1  4742  axrep5  4746  axsep  4750  zfnuleu  4756  axnulALT  4757  vprc  4766  inex1  4769  axpweq  4812  zfpow  4814  axpow2  4815  axpow3  4816  reusv2lem4  4842  nfnid  4867  dtruALT  4870  zfpair2  4878  dtruALT2  4882  ssextss  4893  moabex  4898  dffr2  5049  dfepfr  5069  frinxp  5155  ssrelOLD  5179  ssrel2  5181  eqrelrel  5192  reliun  5210  raliunxp  5231  relop  5242  dmopab3  5307  dm0rn0  5312  reldm0  5313  dffr3  5467  cotrg  5476  issref  5478  asymref  5481  asymref2  5482  intirr  5483  dffr4  5665  sucel  5767  sb8iota  5827  dffun2  5867  dffun3  5868  dffun4  5869  dffun5  5870  dffun6f  5871  dffun7  5884  funopab  5891  funcnv2  5925  funcnv  5926  fun2cnv  5928  fun11  5931  fununi  5932  fnres  5975  mptfnf  5982  fnopabg  5984  brprcneu  6151  dffv2  6238  fvn0ssdmfun  6316  dff13  6477  eqoprab2b  6678  mpt22eqb  6734  ralrnmpt2  6740  zfun  6915  uniex2  6917  funcnvuni  7081  dfer2  7703  fiint  8197  marypha1lem  8299  marypha2lem3  8303  inf2  8480  axinf2  8497  scottexs  8710  scott0s  8711  aceq1  8900  dfac4  8905  dfac7  8914  dfac0  8915  dfac1  8916  dfac10  8919  dfac10c  8920  dfac10b  8921  kmlem4  8935  kmlem12  8943  kmlem14  8945  kmlem15  8946  kmlem16  8947  dfackm  8948  ac6n  9267  axpowndlem3  9381  zfcndrep  9396  zfcndun  9397  zfcndpow  9398  axgroth5  9606  axgroth2  9607  grothpw  9608  axgroth4  9614  grothprim  9616  sstskm  9624  fimaxre3  10930  infm3  10942  nnwos  11715  cotr2g  13665  brtrclfv  13693  trclfvcotr  13700  rpnnen2lem12  14898  isprm2  15338  vdwmc2  15626  pgpfac1  18419  pgpfac  18423  iunocv  19965  2ndcdisj2  21200  hausdiag  21388  rnelfmlem  21696  alexsubALTlem3  21793  cnextfun  21808  itg2leub  23441  mptelee  25709  nmoubi  27515  nmobndseqi  27522  nmobndseqiALT  27523  isch2  27968  isch3  27986  choc0  28073  nmopub  28655  nmfnleub  28672  xfree2  29192  moel  29212  mo5f  29213  nmo  29214  2reuswap2  29217  rmo3f  29224  rmo4fOLD  29225  rabeqsnd  29230  cbvdisjf  29271  disjorf  29278  ssrelf  29309  funcnvmptOLD  29351  funcnvmpt  29352  funcnv5mpt  29353  ballotlem2  30373  bnj89  30548  bnj115  30552  bnj145OLD  30556  bnj538OLD  30571  bnj1143  30622  bnj110  30689  bnj611  30749  bnj864  30753  bnj865  30754  bnj1000  30772  bnj978  30780  bnj1049  30803  bnj1052  30804  bnj1090  30808  bnj1030  30816  bnj1133  30818  bnj1171  30829  bnj1172  30830  bnj1174  30832  bnj1176  30834  bnj1204  30841  bnj1253  30846  bnj1388  30862  bnj1523  30900  axrepprim  31340  axunprim  31341  axpowprim  31342  axinfprim  31344  axacprim  31345  untuni  31347  dffr5  31404  dfon2lem8  31449  dfon2lem9  31450  19.12b  31461  brtxpsd3  31698  dfom5b  31714  dffun10  31716  bj-notalbii  32293  bj-ssbeq  32322  bj-ssb0  32323  bj-ssb1a  32327  bj-ssb1  32328  bj-ax12ssb  32330  bj-ssbn  32336  bj-ssbcom3lem  32345  bj-hbext  32396  bj-nfalt  32397  bj-equsalv  32439  bj-abeq2  32469  bj-abeq1  32470  bj-axrep1  32484  bj-axrep5  32488  bj-axsep  32489  bj-zfpow  32491  ax11-pm2  32519  bj-sbnf  32524  bj-hblem  32549  bj-ralvw  32565  bj-ralcom4  32568  bj-sbeq  32596  bj-nfcf  32620  bj-snsetex  32651  wl-equsalcom  32999  wl-sb8et  33005  wl-2sb6d  33012  wl-alanbii  33022  wl-sb8eut  33030  wl-sbcom3  33043  poimirlem25  33105  poimirlem30  33110  heibor1lem  33279  sbcalfi  33590  mpt2bi123f  33642  mptbi12f  33646  dvelimf-o  33733  axc11n-16  33742  pmapglbx  34574  dford4  37115  rp-fakeinunass  37381  rababg  37399  elmapintrab  37402  elinintrab  37403  undmrnresiss  37430  clss2lem  37438  cotrintab  37441  elintima  37465  ss2iundf  37471  relexp0eq  37513  dfhe3  37590  snhesn  37601  psshepw  37603  dffrege76  37754  frege77  37755  frege110  37788  dffrege115  37793  frege116  37794  frege118  37796  frege131  37809  ntrneikb  37913  ntrneixb  37914  pm10.541  38087  pm10.542  38088  19.21vv  38096  19.31vv  38104  19.28vv  38106  pm11.62  38115  axc11next  38128  pm13.196a  38136  2sbc6g  38137  elnev  38160  conss34OLD  38167  hbexgVD  38664  iunssf  38785  rabssf  38827  2rexsb  40504  2rmoswap  40518  spr0nelg  41044  dffun3f  41751  setrec1lem2  41758  setrec2  41765  alimp-surprise  41859  alimp-no-surprise  41860
  Copyright terms: Public domain W3C validator