Theorem hbra1 1690

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 1005	. 2 |- (A.x(x e. A -> ph) -> A.xA.x(x e. A -> ph))
2		df-ral 1652	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
3	2	albii 1001	. 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 956   e. wcel 960  A.wral 1648

This theorem is referenced by:  r19.12 1743  r19.15 1756  uniiunlem 2135  ralidm 2361  ss2iun 2581  iineq2 2583  hbii1 2589  dfiun2g 2590  ralxfrd 2903  ralxfr 2905  peano5 3159  tfinds 3167  ralxp 3224  zfrep6 3620  fnopabg 3621  elrnopabg 3806  chfnrn 3808  fopab2 3829  ffnfv 3834  isotrALT 3904  iunon 3915  iinon 3916  tfrlem1 3917  tfr3 3932  tz7.48-1 3962  tz7.49 3965  elrnoprabg 4130  nneneq 4518  r1tr 4664  scottex 4726  aceq6b 4752  zorn2lem5 4802  lble 6049  bccl2t 6971  sumeq2 6985  clm4le 7081  clm0 7083  clm0nns 7085  climabs0 7113  climsup 7155  caucvglem6 7162  rnbra 10035  irredt 10317  cmphmp 10507  homcard 10525  imonclem 10712  ismonc 10713  cmpmon 10714

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  df-ral 1652

Copyright terms: Public domain