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

Theorem albii 1640
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 1639 . 2
2 albii.1 . 2
31, 2mpg 1620 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  A.wal 1393
This theorem is referenced by:  2albii  1641  hbxfrbi  1643  nfbii  1644  alex  1647  2nalexn  1649  2exnaln  1650  alinexa  1663  alexn  1664  19.26-2  1681  19.26-3an  1682  19.35OLD  1688  19.43OLD  1694  albiim  1699  2albiim  1700  exintrbi  1701  19.32v  1730  19.31v  1731  19.23vv  1761  pm11.53v  1764  19.12vvv  1765  alrot3  1846  alrot4  1847  19.21-2  1906  equsalhw  1945  19.32  1967  19.31  1968  aaan  1975  pm11.53  1983  19.12vv  1986  equsal  2036  sbcom3  2153  2sb6  2188  2sb6rf  2196  sbex  2207  sbalv  2208  dvelimf-o  2259  axc11n-16  2268  sb8eu  2318  sb8euOLD  2319  eu1  2327  2mo2  2372  2eu1  2376  2eu3  2379  2eu4OLD  2381  exists1  2388  eqcomOLD  2467  hblem  2580  abeq2  2581  abeq1  2582  abbi  2588  nfceqiOLD  2616  abid2fOLD  2649  r2allem  2832  r2alfOLD  2834  r3al  2837  r19.21t  2854  r19.21tOLD  2855  r19.21v  2862  ralbii2  2886  r3alOLD  2895  r19.23t  2935  rabid2  3035  rabbi  3036  ralv  3123  ceqsralt  3133  ralxpxfr2d  3224  ralab  3260  ralrab2  3265  euind  3286  reu2  3287  reu3  3289  rmo4  3292  reu8  3295  rmoim  3299  2reuswap  3302  reuind  3303  2reu5lem2  3306  2reu5lem3  3307  ra4vOLD  3424  ra4OLD  3426  rmo2  3427  rmo3  3429  dfss2  3492  ss2ab  3567  ss2rab  3575  rabss  3576  uniiunlem  3587  ssequn1  3673  unss  3677  ralunb  3684  ssin  3719  n0f  3793  eqv  3801  disj  3867  disj3  3871  ssdif0  3885  inssdif0  3895  ssundif  3911  pwss  4027  ralsnsg  4061  disjsn  4090  euabsn2  4101  snss  4154  pwpw0  4178  pwsnALT  4244  dfnfc2  4267  unissb  4281  elintrab  4298  ssintrab  4310  intun  4319  intpr  4320  dfiin2g  4363  iunss  4371  dfdisj2  4424  cbvdisj  4432  disjor  4436  dftr2  4547  dftr5  4548  trint  4560  axrep1  4564  axrep5  4568  axsep  4572  zfnuleu  4578  axnulALT  4579  vprc  4590  inex1  4593  axpweq  4629  zfpow  4631  axpow2  4632  axpow3  4633  reusv2lem4  4656  nfnid  4681  dtruALT  4684  zfpair2  4692  dtruALT2  4696  ssextss  4706  moabex  4711  dffr2  4849  dfepfr  4869  sucel  4956  frinxp  5070  ssrel  5096  ssrel2  5098  eqrelrel  5109  reliun  5128  raliunxp  5147  relop  5158  dmopab3  5220  dm0rn0  5224  reldm0  5225  dffr3  5374  cotrg  5383  issref  5385  asymref  5388  asymref2  5389  intirr  5390  sb8iota  5563  dffun2  5603  dffun3  5604  dffun4  5605  dffun5  5606  dffun6f  5607  dffun7  5619  funopab  5626  funcnv2  5652  funcnv  5653  fun2cnv  5655  fun11  5658  fununi  5659  fnres  5702  fnopabg  5709  brprcneu  5864  dffv2  5946  fvn0ssdmfun  6022  dff13  6166  eqoprab2b  6355  mpt22eqb  6411  ralrnmpt2  6417  zfun  6593  uniex2  6595  funcnvuni  6753  dfer2  7331  fiint  7817  marypha1lem  7913  marypha2lem3  7917  inf2  8061  axinf2  8078  scottexs  8326  scott0s  8327  aceq1  8519  dfac4  8524  dfac7  8533  dfac0  8534  dfac1  8535  dfac10  8538  dfac10c  8539  dfac10b  8540  kmlem4  8554  kmlem12  8562  kmlem14  8564  kmlem15  8565  kmlem16  8566  dfackm  8567  ac6n  8886  axpowndlem3  8996  axpowndlem3OLD  8997  zfcndrep  9013  zfcndun  9014  zfcndpow  9015  axgroth5  9223  axgroth2  9224  grothpw  9225  axgroth4  9231  grothprim  9233  sstskm  9241  fimaxre3  10517  infm3  10527  nnwos  11178  rpnnen2  13959  isprm2  14225  vdwmc2  14497  pgpfac1  17131  pgpfac  17135  iunocv  18712  2ndcdisj2  19958  hausdiag  20146  rnelfmlem  20453  alexsubALTlem3  20549  cnextfun  20564  itg2leub  22141  mptelee  24198  nmoubi  25687  nmobndseqi  25694  nmobndseqiOLD  25695  isch2  26141  isch3  26159  choc0  26244  nmopub  26827  nmfnleub  26844  xfree2  27364  moel  27382  mo5f  27383  nmo  27384  2reuswap2  27387  rmo3f  27394  rmo4fOLD  27395  abeq2f  27398  rabid2f  27400  cbvdisjf  27434  disjorf  27440  ssrelf  27466  mptfnf  27499  funcnvmptOLD  27509  funcnvmpt  27510  funcnv5mpt  27511  ballotlem2  28427  axrepprim  29074  axunprim  29075  axpowprim  29076  axinfprim  29078  axacprim  29079  untuni  29081  dffr5  29182  dfon2lem8  29222  dfon2lem9  29223  19.12b  29234  predreseq  29259  dffr4  29262  brtxpsd3  29546  dfom5b  29562  dffun10  29564  wl-equsalcom  29995  wl-sb8et  30001  wl-2sb6d  30008  wl-alanbii  30018  wl-sb8eut  30022  wl-sbcom3  30035  heibor1lem  30305  sbcalfi  30519  mpt2bi123f  30571  mptbi12f  30575  n0el  30600  dford4  30971  pm10.541  31272  pm10.542  31273  19.21vv  31281  19.31vv  31289  19.28vv  31291  pm11.62  31300  axc11next  31313  pm13.196a  31321  2sbc6g  31322  elnev  31345  conss34  31351  2rexsb  32175  2rmoswap  32189  rabsssn  32920  alimp-surprise  33195  alimp-no-surprise  33196  hbexgVD  33706  bnj89  33774  bnj115  33778  bnj145OLD  33782  bnj538OLD  33797  bnj1143  33849  bnj110  33916  bnj611  33976  bnj864  33980  bnj865  33981  bnj1000  33999  bnj978  34007  bnj1049  34030  bnj1052  34031  bnj1090  34035  bnj1030  34043  bnj1133  34045  bnj1171  34056  bnj1172  34057  bnj1174  34059  bnj1176  34061  bnj1204  34068  bnj1253  34073  bnj1388  34089  bnj1523  34127  bj-nfn  34219  bj-hbext  34264  bj-nfalt  34265  bj-equsalv  34309  bj-equsalvv  34310  bj-abeq2  34359  bj-abeq1  34360  bj-axrep1  34374  bj-axrep5  34378  bj-axsep  34379  bj-zfpow  34381  ax11-pm2  34409  bj-sbnf  34412  bj-hblem  34425  bj-ralvw  34441  bj-ralcom4  34444  bj-sbeq  34468  bj-nfcf  34492  bj-snsetex  34521  pmapglbx  35493  rp-fakeinunass  37740  elintima  37765  cotr2g  37786  dfhe3  37799  snhesn  37809  psshepw  37811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185
  Copyright terms: Public domain W3C validator