Theorem hbxfrbi 1361

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

Syntax hints:   -> wi 4   <-> wb 98   A.wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  hbbi  1440  hb3or  1441  hb3an  1442  hbs1f  1664  hbs1  1814  hbsbv  1817  hbeu1  1910  sb8euh  1923  hbmo1  1938  hbmo  1939  hbab1  2029  hbab  2031  cleqh  2137  hbxfreq  2144  hbral  2353  hbra1  2354