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

Theorem albii 1736
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 1735 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1714 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wal 1472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195
This theorem is referenced by:  2albii  1737  hbxfrbi  1741  alex  1742  2nalexn  1744  2exnaln  1745  imnang  1757  alexn  1759  nfbii  1769  19.26-2  1786  19.26-3an  1787  19.43OLD  1799  albiim  1805  2albiim  1806  exintrbiOLD  1808  nfbiiOLD  1823  19.32v  1855  19.31v  1856  19.23vv  1889  pm11.53v  1892  19.12vvv  1893  equsalvw  1917  alrot3  2024  alrot4  2025  19.21-2  2064  19.23t  2065  19.32  2087  19.31  2088  equsalhw  2108  aaan  2155  pm11.53  2166  19.12vv  2167  19.21-2OLD  2202  19.23tOLD  2205  equsal  2278  sbcom3  2398  2sb6  2431  2sb6rf  2439  sbex  2450  sbalv  2451  sb8eu  2490  eu1  2497  2mo2  2537  2eu1  2540  2eu3  2542  exists1  2548  hblem  2717  abeq2  2718  abeq1  2719  abbi  2723  abeq2f  2777  r2allem  2920  r3al  2923  r19.21t  2937  r19.21v  2942  ralbii2  2960  r19.23t  3002  rabid2  3095  rabbi  3096  eqvf  3176  abv  3178  ralv  3191  ceqsralt  3201  ralxpxfr2d  3297  ralab  3333  ralrab2  3338  euind  3359  reu2  3360  reu3  3362  rmo4  3365  reu8  3368  rmoim  3373  2reuswap  3376  reuind  3377  2reu5lem2  3380  2reu5lem3  3381  rmo2  3491  rmo3  3493  dfss2  3556  ss2ab  3632  ss2rab  3640  rabss  3641  uniiunlem  3652  ssequn1  3744  unss  3748  ralunb  3755  ssin  3796  eq0f  3883  n0fOLD  3886  ssdif0  3895  inssdif0  3900  ab0  3904  disj  3968  disj3  3972  ssundif  4003  ralf0  4029  pwss  4122  rabsssn  4161  ralsnsg  4162  disjsn  4191  euabsn2  4203  snss  4258  pwpw0  4283  pwsnALT  4361  dfnfc2  4384  dfnfc2OLD  4385  unissb  4399  elintrab  4417  ssintrab  4429  intun  4438  intpr  4439  dfiin2g  4483  iunss  4491  dfdisj2  4549  cbvdisj  4557  disjor  4561  dftr2  4676  dftr5  4677  trint  4690  axrep1  4694  axrep5  4698  axsep  4702  zfnuleu  4708  axnulALT  4709  vprc  4718  inex1  4721  axpweq  4762  zfpow  4764  axpow2  4765  axpow3  4766  reusv2lem4  4792  nfnid  4817  dtruALT  4820  zfpair2  4828  dtruALT2  4832  ssextss  4842  moabex  4847  dffr2  4992  dfepfr  5012  frinxp  5096  ssrel  5119  ssrel2  5121  eqrelrel  5132  reliun  5150  raliunxp  5170  relop  5181  dmopab3  5245  dm0rn0  5249  reldm0  5250  dffr3  5403  cotrg  5412  issref  5414  asymref  5417  asymref2  5418  intirr  5419  dffr4  5598  sucel  5700  sb8iota  5760  dffun2  5799  dffun3  5800  dffun4  5801  dffun5  5802  dffun6f  5803  dffun7  5815  funopab  5822  funcnv2  5856  funcnv  5857  fun2cnv  5859  fun11  5862  fununi  5863  fnres  5906  mptfnf  5913  fnopabg  5915  brprcneu  6080  dffv2  6165  fvn0ssdmfun  6242  dff13  6393  eqoprab2b  6588  mpt22eqb  6644  ralrnmpt2  6650  zfun  6825  uniex2  6827  funcnvuni  6989  dfer2  7607  fiint  8099  marypha1lem  8199  marypha2lem3  8203  inf2  8380  axinf2  8397  scottexs  8610  scott0s  8611  aceq1  8800  dfac4  8805  dfac7  8814  dfac0  8815  dfac1  8816  dfac10  8819  dfac10c  8820  dfac10b  8821  kmlem4  8835  kmlem12  8843  kmlem14  8845  kmlem15  8846  kmlem16  8847  dfackm  8848  ac6n  9167  axpowndlem3  9277  zfcndrep  9292  zfcndun  9293  zfcndpow  9294  axgroth5  9502  axgroth2  9503  grothpw  9504  axgroth4  9510  grothprim  9512  sstskm  9520  fimaxre3  10821  infm3  10833  nnwos  11589  cotr2g  13511  brtrclfv  13539  trclfvcotr  13546  rpnnen2lem12  14741  isprm2  15181  vdwmc2  15469  pgpfac1  18250  pgpfac  18254  iunocv  19791  2ndcdisj2  21017  hausdiag  21205  rnelfmlem  21513  alexsubALTlem3  21610  cnextfun  21625  itg2leub  23251  mptelee  25520  nmoubi  26804  nmobndseqi  26811  nmobndseqiALT  26812  isch2  27257  isch3  27275  choc0  27362  nmopub  27944  nmfnleub  27961  xfree2  28481  moel  28500  mo5f  28501  nmo  28502  2reuswap2  28505  rmo3f  28512  rmo4fOLD  28513  rabid2f  28517  cbvdisjf  28560  disjorf  28567  ssrelf  28598  funcnvmptOLD  28643  funcnvmpt  28644  funcnv5mpt  28645  ballotlem2  29670  bnj89  29834  bnj115  29838  bnj145OLD  29842  bnj538OLD  29857  bnj1143  29908  bnj110  29975  bnj611  30035  bnj864  30039  bnj865  30040  bnj1000  30058  bnj978  30066  bnj1049  30089  bnj1052  30090  bnj1090  30094  bnj1030  30102  bnj1133  30104  bnj1171  30115  bnj1172  30116  bnj1174  30118  bnj1176  30120  bnj1204  30127  bnj1253  30132  bnj1388  30148  bnj1523  30186  axrepprim  30626  axunprim  30627  axpowprim  30628  axinfprim  30630  axacprim  30631  untuni  30633  dffr5  30689  dfon2lem8  30732  dfon2lem9  30733  19.12b  30744  brtxpsd3  30966  dfom5b  30982  dffun10  30984  bj-notalbii  31576  bj-nfn  31588  bj-ssbeq  31609  bj-ssb0  31610  bj-ssb1a  31614  bj-ssb1  31615  bj-ax12ssb  31617  bj-ssbn  31623  bj-ssbcom3lem  31632  bj-hbext  31681  bj-nfalt  31682  bj-equsalv  31724  bj-abeq2  31754  bj-abeq1  31755  bj-axrep1  31769  bj-axrep5  31773  bj-axsep  31774  bj-zfpow  31776  ax11-pm2  31804  bj-sbnf  31809  bj-hblem  31826  bj-ralvw  31842  bj-ralcom4  31845  bj-sbeq  31871  bj-nfcf  31895  bj-snsetex  31927  wl-equsalcom  32290  wl-sb8et  32296  wl-2sb6d  32303  wl-alanbii  32313  wl-sb8eut  32321  wl-sbcom3  32334  poimirlem25  32387  poimirlem30  32392  heibor1lem  32561  sbcalfi  32872  mpt2bi123f  32924  mptbi12f  32928  dvelimf-o  33015  axc11n-16  33024  pmapglbx  33856  dford4  36397  rp-fakeinunass  36663  rababg  36681  elmapintrab  36684  elinintrab  36685  undmrnresiss  36712  clss2lem  36720  cotrintab  36723  elintima  36747  ss2iundf  36753  relexp0eq  36795  dfhe3  36872  snhesn  36883  psshepw  36885  dffrege76  37036  frege77  37037  frege110  37070  dffrege115  37075  frege116  37076  frege118  37078  frege131  37091  ntrneikb  37195  ntrneixb  37196  pm10.541  37371  pm10.542  37372  19.21vv  37380  19.31vv  37388  19.28vv  37390  pm11.62  37399  axc11next  37412  pm13.196a  37420  2sbc6g  37421  elnev  37444  conss34OLD  37450  hbexgVD  37947  iunssf  38073  rabssf  38117  2rexsb  39602  2rmoswap  39616  alimp-surprise  42277  alimp-no-surprise  42278
  Copyright terms: Public domain W3C validator