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

Metamath Proof Explorer

Theorem bj-ax12ssb

Description: Axiom bj-ax12 expressed using substitution. (Contributed by BJ, 26-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ax12ssb 
|- [ t / x ] ( ph -> [ t / x ] ph )

Proof

Step Hyp Ref Expression
1 bj-ax12 
 |-  A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) )
2 sb6 
 |-  ( [ t / x ] ph <-> A. x ( x = t -> ph ) )
3 2 imbi2i 
 |-  ( ( ph -> [ t / x ] ph ) <-> ( ph -> A. x ( x = t -> ph ) ) )
4 3 imbi2i 
 |-  ( ( x = t -> ( ph -> [ t / x ] ph ) ) <-> ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) )
5 4 albii 
 |-  ( A. x ( x = t -> ( ph -> [ t / x ] ph ) ) <-> A. x ( x = t -> ( ph -> A. x ( x = t -> ph ) ) ) )
6 1 5 mpbir 
 |-  A. x ( x = t -> ( ph -> [ t / x ] ph ) )
7 sb6 
 |-  ( [ t / x ] ( ph -> [ t / x ] ph ) <-> A. x ( x = t -> ( ph -> [ t / x ] ph ) ) )
8 6 7 mpbir 
 |-  [ t / x ] ( ph -> [ t / x ] ph )