Theorem hbxfrbi 1483

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 1481	. 2 |- ( A. x ph <-> A. x ps )
4	1, 2, 3	3imtr4i 201	1 |- ( ph -> A. x ph )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  hbbi  1559  hb3or  1560  hb3an  1561  hbs1f  1792  hbs1  1954  hbsbv  1957  hbeu1  2052  sb8euh  2065  hbmo1  2080  hbmo  2081  hbab1  2182  hbab  2184  cleqh  2293  hbxfreq  2300  hbral  2523  hbra1  2524