Metamath Proof Explorer


Theorem bj-sbsb

Description: Biconditional showing two possible (dual) definitions of substitution df-sb not using dummy variables. (Contributed by BJ, 19-Mar-2021)

Ref Expression
Assertion bj-sbsb x = y φ x x = y φ x x = y φ x = y φ

Proof

Step Hyp Ref Expression
1 simpl x = y φ x x = y φ x = y φ
2 pm2.27 x = y x = y φ φ
3 2 anc2li x = y x = y φ x = y φ
4 3 sps x x = y x = y φ x = y φ
5 olc x = y φ x x = y φ x = y φ
6 1 4 5 syl56 x x = y x = y φ x x = y φ x x = y φ x = y φ
7 simpr x = y φ x x = y φ x x = y φ
8 equs5 ¬ x x = y x x = y φ x x = y φ
9 8 biimpd ¬ x x = y x x = y φ x x = y φ
10 orc x x = y φ x x = y φ x = y φ
11 7 9 10 syl56 ¬ x x = y x = y φ x x = y φ x x = y φ x = y φ
12 6 11 pm2.61i x = y φ x x = y φ x x = y φ x = y φ
13 sp x x = y φ x = y φ
14 pm3.4 x = y φ x = y φ
15 13 14 jaoi x x = y φ x = y φ x = y φ
16 equs4 x x = y φ x x = y φ
17 19.8a x = y φ x x = y φ
18 16 17 jaoi x x = y φ x = y φ x x = y φ
19 15 18 jca x x = y φ x = y φ x = y φ x x = y φ
20 12 19 impbii x = y φ x x = y φ x x = y φ x = y φ