Theorem hbxfrbi 1429

Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
hbxfrbi.1	|- ( ph <-> ps )
hbxfrbi.2	|- ( ps -> A. x ps )

Assertion

Ref	Expression
hbxfrbi	|- ( ph -> A. x ph )

Proof of Theorem hbxfrbi

Step	Hyp	Ref	Expression
1		hbxfrbi.2	. 2 |- ( ps -> A. x ps )
2		hbxfrbi.1	. 2 |- ( ph <-> ps )
3	2	albii 1427	. 2 |- ( A. x ph <-> A. x ps )
4	1, 2, 3	3imtr4i 200	1 |- ( ph -> A. x ph )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1310

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  hbbi  1508  hb3or  1509  hb3an  1510  hbs1f  1735  hbs1  1887  hbsbv  1890  hbeu1  1983  sb8euh  1996  hbmo1  2011  hbmo  2012  hbab1  2102  hbab  2104  cleqh  2212  hbxfreq  2219  hbral  2436  hbra1  2437