Theorem hbra1 1237

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 698	. 2 |- (A.x(x e. A -> ph) -> A.xA.x(x e. A -> ph))
2		df-ral 1205	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
3	2	bial 695	. 2 |- (A.xA.x e. A ph <-> A.xA.x(x e. A -> ph))
4	1, 2, 3	3imtr4 192	1 |- (A.x e. A ph -> A.xA.x e. A ph)

Syntax hints:   -> wi 2  A.wal 672   e. wcel 1092  A.wral 1201

This theorem is referenced by:  r19.12 1281  r19.15 1292  ralidm 1774  ss2iun 2005  iineq2 2007  hbii1 2013  peano5 2394  tfinds 2401  ralxp 2456  zfrep6 2744  fnopabg 2745  chfnrn 2885  fopab2 2891  ffnfv 2892  isotrALT 2936  iunon 2947  iinon 2948  tfrlem1 2949  tfr3 2964  tz7.48-1 2994  tz7.49 2997  nneneq 3408  r1tr 3498  scottex 3541  aceq6b 3565  zornlem5 3607

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198  df-ral 1205

metamath.org