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

Metamath Proof Explorer

Theorem sbco3

Description: A composition law for substitution. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 2-Jun-1993) (Proof shortened by Wolf Lammen, 18-Sep-2018) (New usage is discouraged.)

Ref Expression
Assertion sbco3 ⊢ z y y x φ ↔ z x x y φ

Proof

Step Hyp Ref Expression
1 drsb1 ⊢ ∀ x x = y → z x y x φ ↔ z y y x φ
2 nfae ⊢ Ⅎ x ∀ x x = y
3 sbequ12a ⊢ x = y → y x φ ↔ x y φ
4 3 sps ⊢ ∀ x x = y → y x φ ↔ x y φ
5 2 4 sbbid ⊢ ∀ x x = y → z x y x φ ↔ z x x y φ
6 1 5 bitr3d ⊢ ∀ x x = y → z y y x φ ↔ z x x y φ
7 nfnae ⊢ Ⅎ y ¬ ∀ x x = y
8 nfnae ⊢ Ⅎ x ¬ ∀ x x = y
9 nfsb2 ⊢ ¬ ∀ x x = y → Ⅎ x y x φ
10 7 8 9 sbco2d ⊢ ¬ ∀ x x = y → z x x y y x φ ↔ z y y x φ
11 sbco ⊢ x y y x φ ↔ x y φ
12 11 sbbii ⊢ z x x y y x φ ↔ z x x y φ
13 10 12 bitr3di ⊢ ¬ ∀ x x = y → z y y x φ ↔ z x x y φ
14 6 13 pm2.61i ⊢ z y y x φ ↔ z x x y φ