Theorem hbxfrbi 1452

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 1450	. 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 1333

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 1427  ax-gen 1429

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  hbbi  1528  hb3or  1529  hb3an  1530  hbs1f  1761  hbs1  1918  hbsbv  1921  hbeu1  2016  sb8euh  2029  hbmo1  2044  hbmo  2045  hbab1  2146  hbab  2148  cleqh  2257  hbxfreq  2264  hbral  2486  hbra1  2487