Theorem hbxfrbi 1401

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

Syntax hints:   -> wi 4   <-> wb 103   A.wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  hbbi  1480  hb3or  1481  hb3an  1482  hbs1f  1704  hbs1  1855  hbsbv  1858  hbeu1  1951  sb8euh  1964  hbmo1  1979  hbmo  1980  hbab1  2070  hbab  2072  cleqh  2178  hbxfreq  2185  hbral  2395  hbra1  2396