Theorem hbxfrbi 1521

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 1519	. 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 1396

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 1496  ax-gen 1498

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  hbbi  1597  hb3or  1598  hb3an  1599  hbs1f  1830  hbs1  1992  hbsbv  1995  hbeu1  2090  sb8euh  2103  hbmo1  2118  hbmo  2119  hbab1  2221  hbab  2223  cleqh  2332  hbxfreq  2339  hbral  2571  hbra1  2572