Theorem hbxfrbi 1465

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 1463	. 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 1346

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 1440  ax-gen 1442

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  hbbi  1541  hb3or  1542  hb3an  1543  hbs1f  1774  hbs1  1931  hbsbv  1934  hbeu1  2029  sb8euh  2042  hbmo1  2057  hbmo  2058  hbab1  2159  hbab  2161  cleqh  2270  hbxfreq  2277  hbral  2499  hbra1  2500