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

Theorem albii 1896
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 1895 . 2 (∀𝑥(𝜑𝜓) → (∀𝑥𝜑 ↔ ∀𝑥𝜓))
2 albii.1 . 2 (𝜑𝜓)
31, 2mpg 1873 1 (∀𝑥𝜑 ↔ ∀𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197
This theorem is referenced by:  2albii  1897  hbxfrbi  1901  alex  1902  2nalexn  1904  2exnaln  1905  imnang  1918  alexn  1920  nfnbi  1930  19.26-2  1948  19.26-3an  1949  19.43OLD  1960  albiim  1965  2albiim  1966  nfbiiOLD  1985  19.32v  2018  19.31v  2019  19.23vv  2021  pm11.53v  2071  19.12vvv  2072  equsalvw  2086  alrot3  2187  alrot4  2188  19.21-2  2225  19.23t  2226  19.32  2248  19.31  2249  equsalv  2255  equsalhw  2270  aaan  2315  pm11.53  2324  19.12vv  2325  19.21-2OLD  2360  19.23tOLD  2363  equsal  2436  sbcom3  2548  2sb6  2581  2sb6rf  2589  sbex  2600  sbalv  2601  sb8eu  2641  eu1  2648  2mo2  2688  2eu1  2691  2eu3  2693  exists1  2699  hblem  2869  abeq2  2870  abeq1  2871  abbi  2875  abeq2f  2930  r2allem  3075  r3al  3078  r19.21t  3093  r19.21v  3098  ralbii2  3116  r19.23t  3159  rabid2  3257  rabid2f  3258  rabbi  3259  eqvf  3344  abv  3346  ralv  3359  ceqsralt  3369  rspc2gv  3460  ralxpxfr2d  3466  ralab  3508  ralrab2  3513  euind  3534  reu2  3535  reu3  3537  rmo4  3540  reu8  3543  rmoim  3548  2reuswap  3551  reuind  3552  2reu5lem2  3555  2reu5lem3  3556  rmo2  3667  rmo3  3669  dfss2  3732  ss2ab  3811  ss2rab  3819  rabss  3820  uniiunlem  3833  dfdif3  3863  ssequn1  3926  unss  3930  ralunb  3937  ssin  3978  eq0f  4068  n0fOLD  4071  ssdif0  4085  inssdif0  4090  ab0  4094  disj  4160  disj3  4164  ssundif  4196  ralf0  4222  pwss  4319  rabsssn  4359  ralsnsg  4360  disjsn  4390  euabsn2  4404  snssg  4459  pwpw0  4489  pwsnALT  4581  dfnfc2  4606  dfnfc2OLD  4607  unissb  4621  elintrab  4640  ssintrab  4652  intun  4661  intpr  4662  dfiin2g  4705  iunss  4713  dfdisj2  4774  cbvdisj  4782  disjor  4786  dftr2  4906  dftr5  4907  trint  4920  axrep1  4924  axrep5  4928  axsep  4932  zfnuleu  4938  axnulALT  4939  vprc  4948  inex1  4951  axpweq  4991  zfpow  4993  axpow2  4994  axpow3  4995  reusv2lem4  5021  nfnid  5046  dtruALT  5048  zfpair2  5056  dtruALT2  5060  ssextss  5071  moabex  5076  dffr2  5231  dfepfr  5251  frinxp  5341  ssrelOLD  5365  ssrel2  5367  eqrelrel  5378  reliun  5395  raliunxp  5417  relop  5428  dmopab3  5492  dm0rn0  5497  reldm0  5498  dffr3  5656  cotrg  5665  issref  5667  asymref  5670  asymref2  5671  intirr  5672  dffr4  5857  sucel  5959  sb8iota  6019  dffun2  6059  dffun3  6060  dffun4  6061  dffun5  6062  dffun6f  6063  dffun7  6076  funopab  6084  funcnv2  6118  funcnv  6119  fun2cnv  6121  fun11  6124  fununi  6125  fnres  6168  mptfnf  6176  fnopabg  6178  brprcneu  6345  dffv2  6433  fvn0ssdmfun  6513  dff13  6675  eqoprab2b  6878  mpt22eqb  6934  ralrnmpt2  6940  zfun  7115  uniex2  7117  funcnvuni  7284  dfer2  7912  fiint  8402  marypha1lem  8504  marypha2lem3  8508  inf2  8693  axinf2  8710  scottexs  8923  scott0s  8924  aceq1  9130  dfac4  9135  dfac7  9146  dfac0  9147  dfac1  9148  dfac10  9151  dfac10c  9152  dfac10b  9153  kmlem4  9167  kmlem12  9175  kmlem14  9177  kmlem15  9178  kmlem16  9179  dfackm  9180  ac6n  9499  axpowndlem3  9613  zfcndrep  9628  zfcndun  9629  zfcndpow  9630  axgroth5  9838  axgroth2  9839  grothpw  9840  axgroth4  9846  grothprim  9848  sstskm  9856  fimaxre3  11162  infm3  11174  nnwos  11948  cotr2g  13916  brtrclfv  13942  trclfvcotr  13949  rpnnen2lem12  15153  isprm2  15597  vdwmc2  15885  pgpfac1  18679  pgpfac  18683  iunocv  20227  2ndcdisj2  21462  hausdiag  21650  rnelfmlem  21957  alexsubALTlem3  22054  cnextfun  22069  itg2leub  23700  mptelee  25974  nmoubi  27936  nmobndseqi  27943  nmobndseqiALT  27944  isch2  28389  isch3  28407  choc0  28494  nmopub  29076  nmfnleub  29093  xfree2  29613  moel  29632  mo5f  29633  nmo  29634  2reuswap2  29636  rmo3f  29643  rmo4fOLD  29644  rabeqsnd  29649  cbvdisjf  29692  disjorf  29699  ssrelf  29734  funcnvmptOLD  29776  funcnvmpt  29777  funcnv5mpt  29778  ballotlem2  30859  bnj89  31096  bnj115  31100  bnj538OLD  31117  bnj1143  31168  bnj110  31235  bnj611  31295  bnj864  31299  bnj865  31300  bnj1000  31318  bnj978  31326  bnj1049  31349  bnj1052  31350  bnj1090  31354  bnj1030  31362  bnj1133  31364  bnj1171  31375  bnj1172  31376  bnj1174  31378  bnj1176  31380  bnj1204  31387  bnj1253  31392  bnj1388  31408  bnj1523  31446  axrepprim  31886  axunprim  31887  axpowprim  31888  axinfprim  31890  axacprim  31891  untuni  31893  dffr5  31950  elintfv  31969  dfon2lem8  32000  dfon2lem9  32001  19.12b  32012  brtxpsd3  32309  dfom5b  32325  dffun10  32327  bj-notalbii  32904  bj-ssbeq  32933  bj-ssb0  32934  bj-ssb1a  32938  bj-ssb1  32939  bj-ax12ssb  32941  bj-ssbn  32947  bj-ssbcom3lem  32956  bj-hbext  33007  bj-nfalt  33008  bj-abeq2  33079  bj-abeq1  33080  bj-axrep1  33094  bj-axrep5  33098  bj-axsep  33099  bj-zfpow  33101  ax11-pm2  33129  bj-sbnf  33134  bj-hblem  33155  bj-ralvw  33171  bj-ralcom4  33174  bj-sbeq  33202  bj-nfcf  33226  bj-snsetex  33257  bj-raldifsn  33360  wl-equsalcom  33641  wl-sb8et  33647  wl-2sb6d  33654  wl-alanbii  33664  wl-sb8eut  33672  wl-sbcom3  33685  poimirlem25  33747  poimirlem30  33752  heibor1lem  33921  sbcalfi  34232  mpt2bi123f  34284  mptbi12f  34288  ralanid  34335  3albii  34337  ineccnvmo  34445  alrmomorn  34446  cocossss  34514  cossssid3  34542  cossssid4  34543  cosscnvssid4  34550  trcoss2  34557  dvelimf-o  34718  axc11n-16  34727  pmapglbx  35558  dford4  38098  rp-fakeinunass  38363  rababg  38381  elmapintrab  38384  elinintrab  38385  undmrnresiss  38412  clss2lem  38420  cotrintab  38423  elintima  38447  ss2iundf  38453  relexp0eq  38495  dfhe3  38571  snhesn  38582  psshepw  38584  dffrege76  38735  frege77  38736  frege110  38769  dffrege115  38774  frege116  38775  frege118  38777  frege131  38790  ntrneikb  38894  ntrneixb  38895  pm10.541  39068  pm10.542  39069  19.21vv  39077  19.31vv  39085  19.28vv  39087  pm11.62  39096  axc11next  39109  pm13.196a  39117  2sbc6g  39118  elnev  39141  conss34OLD  39148  hbexgVD  39641  iunssf  39762  rabssf  39801  2rexsb  41676  2rmoswap  41690  spr0nelg  42236  dffun3f  42939  setrec1lem2  42945  setrec2  42952  setis  42954  alimp-surprise  43039  alimp-no-surprise  43040
  Copyright terms: Public domain W3C validator