Theorem hbral 1686

Description: Bound-variable hypothesis builder for restricted quantification.

Hypotheses

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

Assertion

Ref	Expression
hbral	|- (A.y e. A ph -> A.xA.y e. A ph)

Distinct variable group:   x,y

Proof of Theorem hbral

Step	Hyp	Ref	Expression
1		hbral.1	. . . 4 |- (y e. A -> A.x y e. A)
2		hbral.2	. . . 4 |- (ph -> A.xph)
3	1, 2	hbim 1007	. . 3 |- ((y e. A -> ph) -> A.x(y e. A -> ph))
4	3	hbal 1005	. 2 |- (A.y(y e. A -> ph) -> A.xA.y(y e. A -> ph))
5		df-ral 1649	. 2 |- (A.y e. A ph <-> A.y(y e. A -> ph))
6	5	albii 999	. 2 |- (A.xA.y e. A ph <-> A.xA.y(y e. A -> ph))
7	4, 5, 6	3imtr4 219	1 |- (A.y e. A ph -> A.xA.y e. A ph)

Syntax hints:   -> wi 3  A.wal 954   e. wcel 958  A.wral 1645

This theorem is referenced by:  tfis 3127  ralxp 3218  ralxpf 3220  f1fvf 3875  hbiso 3892  isotrALT 3898  hbrdg 3936  elrnoprabg 4124  iunfiOLD 4569  scottexs 4718  scott0s 4719  hta 4728  ac6lem 4754  fzrevralt 6519  cau3i 6914  cnlnadjlem5 10004  cmphmp 10521  imonclem 10741  ismonc 10742  cmpmon 10743

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1649

Copyright terms: Public domain