Theorem hbxfrbi 1518

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 1516	. 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 1393

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 1493  ax-gen 1495

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  hbbi  1594  hb3or  1595  hb3an  1596  hbs1f  1827  hbs1  1989  hbsbv  1992  hbeu1  2087  sb8euh  2100  hbmo1  2115  hbmo  2116  hbab1  2218  hbab  2220  cleqh  2329  hbxfreq  2336  hbral  2559  hbra1  2560