Theorem hbra1 1687

Description: x is not free in A.x e. Aph.

Assertion

Ref	Expression
hbra1	|- (A.x e. A ph -> A.xA.x e. A ph)

Proof of Theorem hbra1

Step	Hyp	Ref	Expression
1		hba1 1003	. 2 |- (A.x(x e. A -> ph) -> A.xA.x(x e. A -> ph))
2		df-ral 1649	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
3	2	albii 999	. 2 |- (A.xA.x e. A ph <-> A.xA.x(x e. A -> ph))
4	1, 2, 3	3imtr4 219	1 |- (A.x e. A ph -> A.xA.x e. A ph)

Syntax hints:   -> wi 3  A.wal 954   e. wcel 958  A.wral 1645

This theorem is referenced by:  r19.12 1740  r19.15 1753  uniiunlem 2132  ralidm 2357  ss2iun 2577  iineq2 2579  hbii1 2585  dfiun2g 2586  ralxfrd 2897  ralxfr 2899  peano5 3153  tfinds 3161  ralxp 3218  zfrep6 3614  fnopabg 3615  elrnopabg 3800  chfnrn 3802  fopab2 3823  ffnfv 3828  isotrALT 3898  iunon 3909  iinon 3910  tfrlem1 3911  tfr3 3926  tz7.48-1 3956  tz7.49 3959  elrnoprabg 4124  nneneq 4512  r1tr 4654  scottex 4716  aceq6b 4742  zorn2lem5 4792  lble 6047  bccl2t 6971  sumeq2 6985  clm4le 7081  clm0 7083  clm0nns 7085  climabs0 7113  climsup 7155  caucvglem6 7162  rnbra 10040  irredt 10322  cmphmp 10521  homcard 10539  imonclem 10741  ismonc 10742  cmpmon 10743

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

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

Copyright terms: Public domain