Theorem hbxfrbi 1448

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 1446	. 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 1329

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  hbbi  1527  hb3or  1528  hb3an  1529  hbs1f  1754  hbs1  1911  hbsbv  1914  hbeu1  2009  sb8euh  2022  hbmo1  2037  hbmo  2038  hbab1  2128  hbab  2130  cleqh  2239  hbxfreq  2246  hbral  2464  hbra1  2465