Theorem hbxfrbi 1520

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 1518	. 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 1395

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  hbbi  1596  hb3or  1597  hb3an  1598  hbs1f  1829  hbs1  1991  hbsbv  1994  hbeu1  2089  sb8euh  2102  hbmo1  2117  hbmo  2118  hbab1  2220  hbab  2222  cleqh  2331  hbxfreq  2338  hbral  2561  hbra1  2562