Theorem albii 975

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

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

This theorem is referenced by:  2albii 976  hbex 982  hbor 984  hban 985  hbbi 986  hb3or 987  hb3an 988  hbe1 990  alex 1010  alinexa 1018  exanali 1019  alexn 1020  19.21-2 1033  19.26-2 1044  19.35 1051  19.30 1061  19.32 1062  19.31 1063  19.43 1064  19.41 1071  alrot4 1073  albi 1083  2albi 1084  exintrbi 1094  aaan 1095  equsal 1134  dvelimfALT 1136  dvelimf 1234  sbcom 1242  sb8e 1246  19.23vv 1276  19.12vv 1284  sbcom2 1316  2sb6 1318  sb6a 1319  2sb6rf 1321  sbex 1330  sbalv 1331  2exsb 1333  sbal2 1338  a12lem2 1354  a12studyALT 1356  hbeu1 1365  hbeu 1366  sb8eu 1367  eu1 1369  eu2 1373  hbmo1 1383  hbmo 1384  moanim 1404  2mo 1424  2eu3 1428  2eu4 1429  exists1 1434  hbab1 1443  hbab 1444  hbabd 1445  eqcom 1453  hbxfr 1539  hbeq 1541  hbel 1542  abeq2 1544  abeq1 1545  eq2ab 1549  sbabel 1560  hbne 1620  ralbii2 1647  r2al 1652  hbral 1662  hbra1 1663  hbrex 1664  hbre1 1665  r3al 1666  r19.21t 1691  r19.22 1707  r19.23v 1717  r19.26 1726  hbreu1 1744  rabid2 1746  ralcom2 1752  ralv 1795  reu2 1901  reu6 1903  rmo4 1904  reu8 1907  2reuswap 1908  hbsbc1v 1921  sbcralt 1961  sbcralgf 1963  ra5 1971  hbcsb1g 1995  hbcsbg 1997  dfss2 2029  hbss 2033  ss2ab 2087  ss2rab 2094  rabss 2095  hbdif 2132  hbun 2157  ssequn1 2171  unss 2175  hbin 2191  ne0f 2258  eqv 2266  disj 2282  disj3 2285  ssdif0 2298  inssdif0 2304  ssundif 2315  hbpw 2378  hbpr 2397  ralpr 2399  eusn 2416  snss 2431  pwpw0 2439  prsspw 2450  hbuni 2477  unissb 2496  hbint 2511  elintrab 2513  ssintab 2518  intun 2530  intpr 2531  dfiin2 2556  iunss 2559  ssiun 2560  ssiin 2567  iinss 2568  hbbr 2626  dftr2 2650  dftr5 2651  axrep1 2662  axrep5 2666  axsep 2670  zfnuleu 2675  axnul2 2676  nvelv 2681  inex1 2684  axpow 2711  pwex 2713  sbcsng 2721  ssextss 2730  dtru 2740  zfpair2 2748  hbopab 2774  axun 2831  uniex2 2833  dffr2 2882  dfepfr 2895  hbsuc 3003  sucel 3005  hbxp 3167  weinxp 3195  hbrel 3207  reluni 3227  hbcnv 3252  dmopab3 3279  dm0rn0 3287  reldm0 3288  hbrn 3307  dmcosseq 3316  hbima 3362  dffr3 3382  cotr 3387  intirr 3390  dffun2 3467  dffun3 3468  dffun4 3469  dffun5 3470  dffunmof 3471  hbfun 3477  dffun6 3480  funopab 3488  funcnv2 3496  funcnv 3497  fun2cnv 3499  fun11 3502  fununi 3503  funcnvuni 3504  hbfn 3524  hbf 3565  hbf1 3602  f11 3603  hbfo 3610  hbf1o 3626  fv2 3659  tz6.12-2 3678  fopab2 3762  f1fv 3813  hbiso 3831  tfrlem2 3851  er2 4200  fiint 4486  abfii2 4488  inf2 4532  axinf2 4548  setind2 4573  ranksn 4613  scottexs 4642  scott0s 4643  kardex 4649  karden 4650  aceq1 4653  aceq4 4658  aceq7 4667  ac7 4672  ac6n 4681  kmlem4 4692  kmlem12 4700  kmlem14 4702  kmlem15 4703  kmlem16 4704  aceqkm 4705  axpowndlem3 4874  zfcndrep 4889  zfcndun 4890  zfcndpow 4891  suppsr3 5147  pre-axsup 5214  infm3 5952  infmsup 5966  nnwos 6343  tgss3t 7531  ntreq0 7599  islp2 7636  cncfmet 7792  metcnp4 7852  metcn4 7853  nmobndseqi 8307  axgroth2 8630  axgroth4 8632  grothprim 8635  difeqri2 8703  cnfilca 8801  choc0 9419  h1deot 9601

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-gen 955

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

Copyright terms: Public domain