Theorem albii 996

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

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

This theorem is referenced by:  2albii 997  hbex 1003  hbor 1005  hban 1006  hbbi 1007  hb3or 1008  hb3an 1009  hbe1 1012  alex 1030  alinexa 1038  exanali 1039  alexn 1040  19.21-2 1053  19.26-2 1064  19.35 1071  19.30 1081  19.32 1082  19.31 1083  19.43 1084  19.41 1091  alrot4 1093  albi 1103  2albi 1104  exintrbi 1114  aaan 1115  equsal 1147  dvelimfALT 1149  dvelimf 1245  sbcom 1253  sb8e 1257  19.23vv 1289  19.12vv 1297  sbcom2 1329  2sb6 1331  sb6a 1332  2sb6rf 1334  sbex 1343  sbalv 1344  2exsb 1346  sbal2 1351  a12lem2 1370  a12studyALT 1372  hbeu1 1381  hbeu 1382  sb8eu 1383  eu1 1385  eu2 1389  hbmo1 1399  hbmo 1400  moanim 1420  2mo 1440  2eu3 1444  2eu4 1445  exists1 1450  hbab1 1459  hbab 1460  hbabd 1461  eqcom 1469  hbxfr 1555  hbeq 1557  hbel 1558  abeq2 1560  abeq1 1561  eq2ab 1565  sbabel 1576  hbne 1636  ralbii2 1663  r2al 1668  hbral 1678  hbra1 1679  hbrex 1680  hbre1 1681  r3al 1682  r19.21t 1707  r19.22 1723  r19.23v 1733  r19.26 1742  hbreu1 1760  rabid2 1762  ralcom2 1768  ralv 1811  reu2 1920  reu6 1922  rmo4 1923  reu8 1926  2reuswap 1927  hbsbc1v 1940  sbcralt 1980  sbcralgf 1982  ra5 1990  hbcsb1g 2014  hbcsbg 2016  dfss2 2048  hbss 2052  ss2ab 2106  ss2rab 2113  rabss 2114  hbdif 2151  hbun 2176  ssequn1 2190  unss 2194  hbin 2210  ne0f 2277  eqv 2285  disj 2301  disj3 2304  ssdif0 2317  inssdif0 2323  ssundif 2334  hbpw 2397  hbpr 2416  ralpr 2418  eusn 2436  snss 2452  pwpw0 2460  prsspw 2471  hbuni 2499  unissb 2518  hbint 2533  elintrab 2535  ssintab 2540  intun 2552  intpr 2553  dfiin2 2578  iunss 2581  ssiun 2582  ssiin 2589  iinss 2590  hbbr 2648  dftr2 2672  dftr5 2673  axrep1 2684  axrep5 2688  axsep 2692  zfnuleu 2697  axnul2 2698  nvelv 2703  inex1 2706  axpow 2733  pwex 2735  sbcsng 2743  ssextss 2752  dtru 2762  zfpair2 2770  hbopab 2801  axun 2858  uniex2 2860  dffr2 2909  dfepfr 2922  hbsuc 3030  sucel 3032  hbxp 3194  weinxp 3223  hbrel 3235  reluni 3255  relop 3265  hbcnv 3284  dmopab3 3311  dm0rn0 3319  reldm0 3320  hbrn 3337  dmcosseq 3349  hbima 3395  dffr3 3415  cotr 3420  asymref 3423  asymref2 3424  asymrefOLD 3425  asymref2OLD 3426  intirr 3427  dffun2 3512  dffun3 3513  dffun4 3514  dffun5 3515  dffunmof 3516  hbfun 3522  dffun6 3525  funopab 3534  funcnv2 3542  funcnv 3543  fun2cnv 3545  fun11 3548  fununi 3549  funcnvuni 3550  hbfn 3570  hbf 3611  hbf1 3648  f11 3649  hbfo 3656  hbf1o 3672  fv2 3705  tz6.12-2 3724  fopab2 3808  f1fv 3859  hbiso 3877  tfrlem2 3897  dfer2 4246  fiint 4534  abfii2 4536  inf2 4580  axinf2 4596  setind2 4621  ranksn 4661  scottexs 4690  scott0s 4691  kardex 4697  karden 4698  aceq1 4701  aceq4 4706  aceq7 4715  ac7 4720  ac6n 4729  kmlem4 4740  kmlem12 4748  kmlem14 4750  kmlem15 4751  kmlem16 4752  aceqkm 4753  axpowndlem3 4923  zfcndrep 4938  zfcndun 4939  zfcndpow 4940  suppsr3 5196  pre-axsup 5263  infm3 6001  infmsup 6015  nnwos 6392  tgss3t 7580  ntreq0 7650  islp2 7688  cncfmet 7844  metcnp4 7904  metcn4 7905  nmobndseqi 8372  axgroth2 8717  axgroth4 8719  grothprim 8722  choc0 9205  h1deot 9387  difeqri2 10344  cnfilca 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972

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

Copyright terms: Public domain