Theorem albii 1040

Description: Inference adding universal quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
albii.1	|- (ph <-> ps)

Assertion

Ref	Expression
albii	|- (A.xph <-> A.xps)

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		19.15 1038	. 2 |- (A.x(ph <-> ps) -> (A.xph <-> A.xps))
2		albii.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 1027	1 |- (A.xph <-> A.xps)

Syntax hints:   <-> wb 153  A.wal 995

This theorem is referenced by:  2albii 1041  hbex 1047  hbor 1049  hban 1050  hbbi 1051  hb3or 1052  hb3an 1053  hbe1 1057  alex 1075  alinexa 1083  exanali 1084  alexn 1085  19.21-2 1098  19.26-2 1109  19.35 1116  19.30 1126  19.32 1127  19.31 1128  19.43 1129  19.41 1136  alrot4 1138  albi 1148  2albi 1149  exintrbi 1159  aaan 1160  equsal 1193  dvelimfALT 1195  dvelimf 1292  sbcom 1300  sb8e 1304  19.23vv 1336  19.12vv 1344  sbcom2 1376  2sb6 1378  sb6a 1379  2sb6rf 1381  sbex 1390  sbalv 1391  2exsb 1393  dvelimALT 1395  sbal2 1400  a12lem2 1419  a12studyALT 1421  hbeu1 1430  hbeu 1431  sb8eu 1432  eu1 1434  eu2 1438  hbmo1 1448  hbmo 1449  moanim 1469  2mo 1490  2eu3 1494  2eu4 1495  exists1 1502  hbab1 1512  hbab 1513  hbabd 1514  eqcom 1524  hbxfr 1610  hbeq 1612  hbel 1613  abeq2 1615  abeq1 1616  eq2ab 1620  sbabel 1631  hbne 1691  ralbii2 1718  r2al 1723  hbral 1733  hbra1 1734  hbrex 1735  hbre1 1736  r3al 1737  r19.21t 1762  r19.22 1778  r19.23v 1788  r19.26 1797  hbreu1 1815  rabid2 1817  ralcom2 1823  ralv 1867  reu2 1977  reu6 1979  rmo4 1980  reu8 1983  2reuswap 1984  hbsbc1v 1997  sbcralt 2040  sbcralgf 2042  ra5 2050  hbcsb1g 2075  hbcsbg 2077  dfss2 2109  hbss 2113  ss2ab 2167  ss2rab 2174  rabss 2175  hbdif 2212  hbun 2237  ssequn1 2251  unss 2255  hbin 2271  ne0f 2339  eqv 2347  disj 2363  disj3 2366  ssdif0 2379  inssdif0 2385  ssundif 2396  hbpw 2459  hbpr 2478  ralpr 2480  eusn 2498  snss 2515  pwpw0 2523  prsspw 2534  pwsnALT 2555  hbuni 2563  unissb 2582  hbint 2597  elintrab 2599  ssintab 2604  intun 2616  intpr 2617  dfiin2 2642  iunss 2645  ssiun 2646  ssiin 2653  iinss 2654  hbbr 2713  dftr2 2737  dftr5 2738  axrep1 2749  axrep5 2753  axsep 2757  zfnuleu 2762  axnul2 2763  vprc 2768  inex1 2771  axpow 2799  pwex 2801  sbcsng 2809  ssextss 2818  dtru 2828  zfpair2 2836  hbopab 2868  axun 2923  uniex2 2925  dffr2 2976  dfepfr 2989  hbsuc 3097  sucel 3099  hbxp 3261  weinxp 3290  hbrel 3302  reluni 3322  relop 3332  hbcnv 3352  dmopab3 3379  dm0rn0 3387  reldm0 3388  hbrn 3408  dmcosseq 3422  hbima 3468  dffr3 3488  cotr 3493  asymref 3496  asymref2 3497  intirr 3498  dffun2 3583  dffun3 3584  dffun4 3585  dffun5 3586  dffunmof 3587  hbfun 3593  dffun6 3596  funopab 3605  funcnv2 3613  funcnv 3614  fun2cnv 3616  fun11 3619  fununi 3620  funcnvuni 3621  hbfn 3641  hbf 3682  hbf1 3720  f11 3721  hbfo 3728  hbf1o 3744  fv2 3777  tz6.12-2 3796  fopab2 3880  f1fv 3931  hbiso 3950  tfrlem2 3970  dfer2 4320  fiint 4620  abfii2 4622  inf2 4670  axinf2 4686  setind2 4711  ranksn 4751  scottexs 4780  scott0s 4781  kardex 4787  karden 4788  aceq1 4791  aceq4 4796  aceq7 4805  ac7 4810  ac6n 4819  kmlem4 4830  kmlem12 4838  kmlem14 4840  kmlem15 4841  kmlem16 4842  aceqkm 4843  axpowndlem3 5016  zfcndrep 5031  zfcndun 5032  zfcndpow 5033  suppsr3 5289  pre-axsup 5356  infm3 6136  infmsup 6150  nnwos 6486  tgss3 7727  ntreq0 7793  islp2 7832  cncfmet 7990  metcnp4 8055  metcn4 8056  nmobndseqi 8524  spwpr2 8742  axgroth2 8861  axgroth4 8863  grothprim 8866  choc0 9373  h1deoi 9555  difeqri2 10529  ref3w 10566  cnfilca 10670  usinuniop 10703

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232

Copyright terms: Public domain