Theorem hbxfrbi 1482

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 1480	. 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 1361

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 1457  ax-gen 1459

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  hbbi  1558  hb3or  1559  hb3an  1560  hbs1f  1791  hbs1  1949  hbsbv  1952  hbeu1  2047  sb8euh  2060  hbmo1  2075  hbmo  2076  hbab1  2177  hbab  2179  cleqh  2288  hbxfreq  2295  hbral  2518  hbra1  2519