Theorem hbre1 1689

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

Assertion

Ref	Expression
hbre1	|- (E.x e. A ph -> A.xE.x e. A ph)

Proof of Theorem hbre1

Step	Hyp	Ref	Expression
1		hbe1 1016	. 2 |- (E.x(x e. A /\ ph) -> A.xE.x(x e. A /\ ph))
2		df-rex 1650	. 2 |- (E.x e. A ph <-> E.x(x e. A /\ ph))
3	2	albii 999	. 2 |- (A.xE.x e. A ph <-> A.xE.x(x e. A /\ ph))
4	1, 2, 3	3imtr4 219	1 |- (E.x e. A ph -> A.xE.x e. A ph)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 954   e. wcel 958  E.wex 980  E.wrex 1646

This theorem is referenced by:  uniiunlem 2132  hbiu1 2584  onfr 2986  oarec 4196  iunfiOLD 4569  zfregcl 4595  scott0 4717  cncnplem2 7775  chcmh 9113  atom1d 10280  fgsb 10570  fgsbOLD 10571  fgsb2 10580

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  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain