Theorem hbrex 2149

Description: Bound-variable hypothesis builder for restricted quantification. (Unnecessary distinct variable restrictions were removed by David Abernethy, 13-Dec-2009.)

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)

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 1356	. . 3 |- ((y e. A /\ ph) -> A.x(y e. A /\ ph))
4	3	hbex 1353	. 2 |- (E.y(y e. A /\ ph) -> A.xE.y(y e. A /\ ph))
5		df-rex 2110	. 2 |- (E.y e. A ph <-> E.y(y e. A /\ ph))
6	5	albii 1346	. 2 |- (A.xE.y e. A ph <-> A.xE.y(y e. A /\ ph))
7	4, 5, 6	3imtr4i 236	1 |- (E.y e. A ph -> A.xE.y e. A ph)

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   e. wcel 1300  E.wex 1326  E.wrex 2106

This theorem is referenced by:  r19.12 2204  r19.12OLD 2205  sbcrexg 2533  iunrab 3299  eufromeq5 3832  abrexexlem2 4835  abrexex2 4847  elrnoprabg 5066  hbrdg 5144  oarec 5244  hbsum1 8243  hbsum 8244  indexfi 10174  bnj1366 13091  bnj873 13317  bnj1014 13374  bnj1123 13422  bnj1307 13488  bnj1313 13494  bnj1445 13535  bnj1446 13536  bnj1467 13549  bnj1463 13550  bnj1499 13561  trcllem1 13933  hbprod1 14659  hbprod 14660  fgsb 14921  fgsb2 14925  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  abrexex2g 15738  indexa 15753  indexfiOLD 15755  filbcmb 15776  sdclem2 15810  sdc 15811  fdc1 15813

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-rex 2110

Copyright terms: Public domain