Theorem hbrex 1687

Description: Bound-variable hypothesis builder for restricted quantification.

Hypotheses

Ref	Expression
hbrex.1	|- (y e. A -> A.x y e. A)
hbrex.2	|- (ph -> A.xph)

Assertion

Ref	Expression
hbrex	|- (E.y e. A ph -> A.xE.y e. A ph)

Distinct variable group:   x,y

Proof of Theorem hbrex

Step	Hyp	Ref	Expression
1		hbrex.1	. . . 4 |- (y e. A -> A.x y e. A)
2		hbrex.2	. . . 4 |- (ph -> A.xph)
3	1, 2	hban 1008	. . 3 |- ((y e. A /\ ph) -> A.x(y e. A /\ ph))
4	3	hbex 1005	. 2 |- (E.y(y e. A /\ ph) -> A.xE.y(y e. A /\ ph))
5		df-rex 1649	. 2 |- (E.y e. A ph <-> E.y(y e. A /\ ph))
6	5	albii 998	. 2 |- (A.xE.y e. A ph <-> A.xE.y(y e. A /\ ph))
7	4, 5, 6	3imtr4 219	1 |- (E.y e. A ph -> A.xE.y e. A ph)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 953   e. wcel 957  E.wex 979  E.wrex 1645

This theorem is referenced by:  r19.12 1739  iunrab 2593  abrexexlem2 3856  abrexex2 3868  hbrdg 3933  elrnoprabg 4121  oarec 4193  hbsum1 6951  hbsum 6952  fgsb 10538  fgsb2 10543

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-4 972  ax-5o 974  ax-6o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-rex 1649

Copyright terms: Public domain