Theorem albii 1001

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 999	. 2 |- (A.x(ph <-> ps) -> (A.xph <-> A.xps))
2		albii.1	. 2 |- (ph <-> ps)
3	1, 2	mpg 988	1 |- (A.xph <-> A.xps)

Syntax hints:   <-> wb 146  A.wal 956

This theorem is referenced by:  2albii 1002  hbex 1008  hbor 1010  hban 1011  hbbi 1012  hb3or 1013  hb3an 1014  hbe1 1018  alex 1036  alinexa 1044  exanali 1045  alexn 1046  19.21-2 1059  19.26-2 1070  19.35 1077  19.30 1087  19.32 1088  19.31 1089  19.43 1090  19.41 1097  alrot4 1099  albi 1109  2albi 1110  exintrbi 1120  aaan 1121  equsal 1153  dvelimfALT 1155  dvelimf 1252  sbcom 1260  sb8e 1264  19.23vv 1296  19.12vv 1304  sbcom2 1336  2sb6 1338  sb6a 1339  2sb6rf 1341  sbex 1350  sbalv 1351  2exsb 1353  dvelimALT 1355  sbal2 1360  a12lem2 1379  a12studyALT 1381  hbeu1 1390  hbeu 1391  sb8eu 1392  eu1 1394  eu2 1398  hbmo1 1408  hbmo 1409  moanim 1429  2mo 1450  2eu3 1454  2eu4 1455  exists1 1460  hbab1 1469  hbab 1470  hbabd 1471  eqcom 1480  hbxfr 1566  hbeq 1568  hbel 1569  abeq2 1571  abeq1 1572  eq2ab 1576  sbabel 1587  hbne 1647  ralbii2 1674  r2al 1679  hbral 1689  hbra1 1690  hbrex 1691  hbre1 1692  r3al 1693  r19.21t 1718  r19.22 1734  r19.23v 1744  r19.26 1753  hbreu1 1771  rabid2 1773  ralcom2 1779  ralv 1823  reu2 1933  reu6 1935  rmo4 1936  reu8 1939  2reuswap 1940  hbsbc1v 1953  sbcralt 1994  sbcralgf 1996  ra5 2004  hbcsb1g 2028  hbcsbg 2030  dfss2 2062  hbss 2066  ss2ab 2120  ss2rab 2127  rabss 2128  hbdif 2165  hbun 2190  ssequn1 2204  unss 2208  hbin 2224  ne0f 2292  eqv 2300  disj 2316  disj3 2319  ssdif0 2332  inssdif0 2338  ssundif 2349  hbpw 2412  hbpr 2431  ralpr 2433  eusn 2451  snss 2466  pwpw0 2474  prsspw 2485  pwsnALT 2506  hbuni 2514  unissb 2533  hbint 2548  elintrab 2550  ssintab 2555  intun 2567  intpr 2568  dfiin2 2593  iunss 2596  ssiun 2597  ssiin 2604  iinss 2605  hbbr 2664  dftr2 2688  dftr5 2689  axrep1 2700  axrep5 2704  axsep 2708  zfnuleu 2713  axnul2 2714  nvelv 2719  inex1 2722  axpow 2750  pwex 2752  sbcsng 2760  ssextss 2769  dtru 2779  zfpair2 2787  hbopab 2819  axun 2874  uniex2 2876  dffr2 2926  dfepfr 2939  hbsuc 3047  sucel 3049  hbxp 3211  weinxp 3240  hbrel 3252  reluni 3272  relop 3282  hbcnv 3302  dmopab3 3329  dm0rn0 3337  reldm0 3338  hbrn 3358  dmcosseq 3372  hbima 3418  dffr3 3438  cotr 3443  asymref 3446  asymref2 3447  intirr 3448  dffun2 3533  dffun3 3534  dffun4 3535  dffun5 3536  dffunmof 3537  hbfun 3543  dffun6 3546  funopab 3555  funcnv2 3563  funcnv 3564  fun2cnv 3566  fun11 3569  fununi 3570  funcnvuni 3571  hbfn 3591  hbf 3632  hbf1 3670  f11 3671  hbfo 3678  hbf1o 3694  fv2 3727  tz6.12-2 3746  fopab2 3830  f1fv 3881  hbiso 3899  tfrlem2 3919  dfer2 4269  fiint 4576  fiintOLD 4577  abfii2 4580  inf2 4624  axinf2 4640  setind2 4666  ranksn 4706  scottexs 4735  scott0s 4736  kardex 4742  karden 4743  aceq1 4746  aceq4 4751  aceq7 4760  ac7 4765  ac6n 4774  kmlem4 4785  kmlem12 4793  kmlem14 4795  kmlem15 4796  kmlem16 4797  aceqkm 4798  axpowndlem3 4970  zfcndrep 4985  zfcndun 4986  zfcndpow 4987  suppsr3 5243  pre-axsup 5310  infm3 6063  infmsup 6077  nnwos 6468  tgss3t 7644  ntreq0 7712  islp2 7751  cncfmet 7909  metcnp4 7974  metcn4 7975  nmobndseqi 8443  spwpr2 8661  axgroth2 8780  axgroth4 8782  grothprim 8785  choc0 9292  h1deot 9474  difeqri2 10446  cnfilca 10570

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain