Metamath Proof Explorer

Theorem bj-sbeq

Description: Distribute proper substitution through an equality relation. (See sbceqg ). (Contributed by BJ, 6-Oct-2018)

Ref Expression
Assertion bj-sbeq ⊢ y x A = B ↔ ⦋ y / x⦌ A = ⦋ y / x⦌ B

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ A = B ↔ ∀ z z ∈ A ↔ z ∈ B
2 1 sbbii ⊢ y x A = B ↔ y x ∀ z z ∈ A ↔ z ∈ B
3 sbsbc ⊢ y x ∀ z z ∈ A ↔ z ∈ B ↔ [˙y / x]˙ ∀ z z ∈ A ↔ z ∈ B
4 sbcal ⊢ [˙y / x]˙ ∀ z z ∈ A ↔ z ∈ B ↔ ∀ z [˙y / x]˙ z ∈ A ↔ z ∈ B
5 2 3 4 3bitri ⊢ y x A = B ↔ ∀ z [˙y / x]˙ z ∈ A ↔ z ∈ B
6 sbcbig ⊢ y ∈ V → [˙y / x]˙ z ∈ A ↔ z ∈ B ↔ [˙y / x]˙ z ∈ A ↔ [˙y / x]˙ z ∈ B
7 6 elv ⊢ [˙y / x]˙ z ∈ A ↔ z ∈ B ↔ [˙y / x]˙ z ∈ A ↔ [˙y / x]˙ z ∈ B
8 7 albii ⊢ ∀ z [˙y / x]˙ z ∈ A ↔ z ∈ B ↔ ∀ z [˙y / x]˙ z ∈ A ↔ [˙y / x]˙ z ∈ B
9 sbcel2 ⊢ [˙y / x]˙ z ∈ A ↔ z ∈ ⦋ y / x⦌ A
10 sbcel2 ⊢ [˙y / x]˙ z ∈ B ↔ z ∈ ⦋ y / x⦌ B
11 9 10 bibi12i ⊢ [˙y / x]˙ z ∈ A ↔ [˙y / x]˙ z ∈ B ↔ z ∈ ⦋ y / x⦌ A ↔ z ∈ ⦋ y / x⦌ B
12 11 albii ⊢ ∀ z [˙y / x]˙ z ∈ A ↔ [˙y / x]˙ z ∈ B ↔ ∀ z z ∈ ⦋ y / x⦌ A ↔ z ∈ ⦋ y / x⦌ B
13 5 8 12 3bitri ⊢ y x A = B ↔ ∀ z z ∈ ⦋ y / x⦌ A ↔ z ∈ ⦋ y / x⦌ B
14 dfcleq ⊢ ⦋ y / x⦌ A = ⦋ y / x⦌ B ↔ ∀ z z ∈ ⦋ y / x⦌ A ↔ z ∈ ⦋ y / x⦌ B
15 13 14 bitr4i ⊢ y x A = B ↔ ⦋ y / x⦌ A = ⦋ y / x⦌ B