This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sb6x

Description: Equivalence involving substitution for a variable not free. Usage of this theorem is discouraged because it depends on ax-13 . Usage of sb6 is preferred, which requires fewer axioms. (Contributed by NM, 2-Jun-1993) (Revised by Mario Carneiro, 4-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypothesis sb6x.1 
|- F/ x ph
Assertion sb6x 
|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )

Proof

Step Hyp Ref Expression
1 sb6x.1 
 |-  F/ x ph
2 1 sbf 
 |-  ( [ y / x ] ph <-> ph )
3 biidd 
 |-  ( x = y -> ( ph <-> ph ) )
4 1 3 equsal 
 |-  ( A. x ( x = y -> ph ) <-> ph )
5 2 4 bitr4i 
 |-  ( [ y / x ] ph <-> A. x ( x = y -> ph ) )