Theorem hbxfrbi 1402

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

Syntax hints:   -> wi 4   <-> wb 103   A.wal 1283

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  hbbi  1481  hb3or  1482  hb3an  1483  hbs1f  1705  hbs1  1856  hbsbv  1859  hbeu1  1952  sb8euh  1965  hbmo1  1980  hbmo  1981  hbab1  2071  hbab  2073  cleqh  2179  hbxfreq  2186  hbral  2396  hbra1  2397