Theorem hbxfrbi 1460

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 1458	. 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 1341

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 1435  ax-gen 1437

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  hbbi  1536  hb3or  1537  hb3an  1538  hbs1f  1769  hbs1  1926  hbsbv  1929  hbeu1  2024  sb8euh  2037  hbmo1  2052  hbmo  2053  hbab1  2154  hbab  2156  cleqh  2266  hbxfreq  2273  hbral  2495  hbra1  2496