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

Theorem albii 1737
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 1736 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1715 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wal 1473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196
This theorem is referenced by:  2albii  1738  hbxfrbi  1742  alex  1743  2nalexn  1745  2exnaln  1746  imnang  1758  alexn  1760  nfbii  1770  19.26-2  1787  19.26-3an  1788  19.43OLD  1800  albiim  1806  2albiim  1807  exintrbiOLD  1809  nfbiiOLD  1824  19.32v  1856  19.31v  1857  19.23vv  1890  pm11.53v  1893  19.12vvv  1894  equsalvw  1918  alrot3  2025  alrot4  2026  19.21-2  2065  19.23t  2066  19.32  2088  19.31  2089  equsalhw  2109  aaan  2156  pm11.53  2167  19.12vv  2168  19.21-2OLD  2203  19.23tOLD  2206  equsal  2279  sbcom3  2399  2sb6  2432  2sb6rf  2440  sbex  2451  sbalv  2452  sb8eu  2491  eu1  2498  2mo2  2538  2eu1  2541  2eu3  2543  exists1  2549  hblem  2718  abeq2  2719  abeq1  2720  abbi  2724  abeq2f  2778  r2allem  2921  r3al  2924  r19.21t  2938  r19.21v  2943  ralbii2  2961  r19.23t  3003  rabid2  3096  rabbi  3097  eqvf  3177  abv  3179  ralv  3192  ceqsralt  3202  ralxpxfr2d  3298  ralab  3334  ralrab2  3339  euind  3360  reu2  3361  reu3  3363  rmo4  3366  reu8  3369  rmoim  3374  2reuswap  3377  reuind  3378  2reu5lem2  3381  2reu5lem3  3382  rmo2  3492  rmo3  3494  dfss2  3557  ss2ab  3633  ss2rab  3641  rabss  3642  uniiunlem  3653  ssequn1  3745  unss  3749  ralunb  3756  ssin  3797  eq0f  3884  n0fOLD  3887  ssdif0  3896  inssdif0  3901  ab0  3905  disj  3969  disj3  3973  ssundif  4004  ralf0  4030  pwss  4123  rabsssn  4162  ralsnsg  4163  disjsn  4192  euabsn2  4204  snss  4259  pwpw0  4284  pwsnALT  4367  dfnfc2  4390  dfnfc2OLD  4391  unissb  4405  elintrab  4423  ssintrab  4435  intun  4444  intpr  4445  dfiin2g  4489  iunss  4497  dfdisj2  4555  cbvdisj  4563  disjor  4567  dftr2  4682  dftr5  4683  trint  4696  axrep1  4700  axrep5  4704  axsep  4708  zfnuleu  4714  axnulALT  4715  vprc  4724  inex1  4727  axpweq  4768  zfpow  4770  axpow2  4771  axpow3  4772  reusv2lem4  4798  nfnid  4823  dtruALT  4826  zfpair2  4834  dtruALT2  4838  ssextss  4849  moabex  4854  dffr2  5003  dfepfr  5023  frinxp  5107  ssrelOLD  5131  ssrel2  5133  eqrelrel  5144  reliun  5162  raliunxp  5183  relop  5194  dmopab3  5259  dm0rn0  5263  reldm0  5264  dffr3  5417  cotrg  5426  issref  5428  asymref  5431  asymref2  5432  intirr  5433  dffr4  5613  sucel  5715  sb8iota  5775  dffun2  5814  dffun3  5815  dffun4  5816  dffun5  5817  dffun6f  5818  dffun7  5830  funopab  5837  funcnv2  5871  funcnv  5872  fun2cnv  5874  fun11  5877  fununi  5878  fnres  5921  mptfnf  5928  fnopabg  5930  brprcneu  6096  dffv2  6181  fvn0ssdmfun  6258  dff13  6416  eqoprab2b  6611  mpt22eqb  6667  ralrnmpt2  6673  zfun  6848  uniex2  6850  funcnvuni  7012  dfer2  7630  fiint  8122  marypha1lem  8222  marypha2lem3  8226  inf2  8403  axinf2  8420  scottexs  8633  scott0s  8634  aceq1  8823  dfac4  8828  dfac7  8837  dfac0  8838  dfac1  8839  dfac10  8842  dfac10c  8843  dfac10b  8844  kmlem4  8858  kmlem12  8866  kmlem14  8868  kmlem15  8869  kmlem16  8870  dfackm  8871  ac6n  9190  axpowndlem3  9300  zfcndrep  9315  zfcndun  9316  zfcndpow  9317  axgroth5  9525  axgroth2  9526  grothpw  9527  axgroth4  9533  grothprim  9535  sstskm  9543  fimaxre3  10849  infm3  10861  nnwos  11631  cotr2g  13563  brtrclfv  13591  trclfvcotr  13598  rpnnen2lem12  14793  isprm2  15233  vdwmc2  15521  pgpfac1  18302  pgpfac  18306  iunocv  19844  2ndcdisj2  21070  hausdiag  21258  rnelfmlem  21566  alexsubALTlem3  21663  cnextfun  21678  itg2leub  23307  mptelee  25575  nmoubi  27011  nmobndseqi  27018  nmobndseqiALT  27019  isch2  27464  isch3  27482  choc0  27569  nmopub  28151  nmfnleub  28168  xfree2  28688  moel  28707  mo5f  28708  nmo  28709  2reuswap2  28712  rmo3f  28719  rmo4fOLD  28720  rabid2f  28724  cbvdisjf  28767  disjorf  28774  ssrelf  28805  funcnvmptOLD  28850  funcnvmpt  28851  funcnv5mpt  28852  ballotlem2  29877  bnj89  30041  bnj115  30045  bnj145OLD  30049  bnj538OLD  30064  bnj1143  30115  bnj110  30182  bnj611  30242  bnj864  30246  bnj865  30247  bnj1000  30265  bnj978  30273  bnj1049  30296  bnj1052  30297  bnj1090  30301  bnj1030  30309  bnj1133  30311  bnj1171  30322  bnj1172  30323  bnj1174  30325  bnj1176  30327  bnj1204  30334  bnj1253  30339  bnj1388  30355  bnj1523  30393  axrepprim  30833  axunprim  30834  axpowprim  30835  axinfprim  30837  axacprim  30838  untuni  30840  dffr5  30896  dfon2lem8  30939  dfon2lem9  30940  19.12b  30951  brtxpsd3  31173  dfom5b  31189  dffun10  31191  bj-notalbii  31783  bj-nfn  31795  bj-ssbeq  31816  bj-ssb0  31817  bj-ssb1a  31821  bj-ssb1  31822  bj-ax12ssb  31824  bj-ssbn  31830  bj-ssbcom3lem  31839  bj-hbext  31888  bj-nfalt  31889  bj-equsalv  31931  bj-abeq2  31961  bj-abeq1  31962  bj-axrep1  31976  bj-axrep5  31980  bj-axsep  31981  bj-zfpow  31983  ax11-pm2  32011  bj-sbnf  32016  bj-hblem  32043  bj-ralvw  32059  bj-ralcom4  32062  bj-sbeq  32088  bj-nfcf  32112  bj-snsetex  32144  wl-equsalcom  32507  wl-sb8et  32513  wl-2sb6d  32520  wl-alanbii  32530  wl-sb8eut  32538  wl-sbcom3  32551  poimirlem25  32604  poimirlem30  32609  heibor1lem  32778  sbcalfi  33089  mpt2bi123f  33141  mptbi12f  33145  dvelimf-o  33232  axc11n-16  33241  pmapglbx  34073  dford4  36614  rp-fakeinunass  36880  rababg  36898  elmapintrab  36901  elinintrab  36902  undmrnresiss  36929  clss2lem  36937  cotrintab  36940  elintima  36964  ss2iundf  36970  relexp0eq  37012  dfhe3  37089  snhesn  37100  psshepw  37102  dffrege76  37253  frege77  37254  frege110  37287  dffrege115  37292  frege116  37293  frege118  37295  frege131  37308  ntrneikb  37412  ntrneixb  37413  pm10.541  37588  pm10.542  37589  19.21vv  37597  19.31vv  37605  19.28vv  37607  pm11.62  37616  axc11next  37629  pm13.196a  37637  2sbc6g  37638  elnev  37661  conss34OLD  37667  hbexgVD  38164  iunssf  38290  rabssf  38334  2rexsb  39819  2rmoswap  39833  dffun3f  42227  setrec1lem2  42234  setrec2  42241  alimp-surprise  42335  alimp-no-surprise  42336
  Copyright terms: Public domain W3C validator