Metamath Proof Explorer

Theorem bj-sbceqgALT

Description: Distribute proper substitution through an equality relation. Alternate proof of sbceqg . (Contributed by BJ, 6-Oct-2018) Proof modification is discouraged to avoid using sbceqg , but the Metamath program "MM-PA> MINIMIZE__WITH * / EXCEPT sbceqg" command is ok. (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-sbceqgALT ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ⦋ A / x⦌ B = ⦋ A / x⦌ C

Proof

Step Hyp Ref Expression
1 dfcleq ⊢ B = C ↔ ∀ y y ∈ B ↔ y ∈ C
2 1 sbcth ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ∀ y y ∈ B ↔ y ∈ C
3 sbcbig ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ∀ y y ∈ B ↔ y ∈ C ↔ [˙A / x]˙ B = C ↔ [˙A / x]˙ ∀ y y ∈ B ↔ y ∈ C
4 2 3 mpbid ⊢ A ∈ V → [˙A / x]˙ B = C ↔ [˙A / x]˙ ∀ y y ∈ B ↔ y ∈ C
5 sbcal ⊢ [˙A / x]˙ ∀ y y ∈ B ↔ y ∈ C ↔ ∀ y [˙A / x]˙ y ∈ B ↔ y ∈ C
6 4 5 bitrdi ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ∀ y [˙A / x]˙ y ∈ B ↔ y ∈ C
7 sbcbig ⊢ A ∈ V → [˙A / x]˙ y ∈ B ↔ y ∈ C ↔ [˙A / x]˙ y ∈ B ↔ [˙A / x]˙ y ∈ C
8 7 albidv ⊢ A ∈ V → ∀ y [˙A / x]˙ y ∈ B ↔ y ∈ C ↔ ∀ y [˙A / x]˙ y ∈ B ↔ [˙A / x]˙ y ∈ C
9 sbcel2 ⊢ [˙A / x]˙ y ∈ B ↔ y ∈ ⦋ A / x⦌ B
10 9 a1i ⊢ A ∈ V → [˙A / x]˙ y ∈ B ↔ y ∈ ⦋ A / x⦌ B
11 sbcel2 ⊢ [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ C
12 11 a1i ⊢ A ∈ V → [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ C
13 10 12 bibi12d ⊢ A ∈ V → [˙A / x]˙ y ∈ B ↔ [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ B ↔ y ∈ ⦋ A / x⦌ C
14 13 albidv ⊢ A ∈ V → ∀ y [˙A / x]˙ y ∈ B ↔ [˙A / x]˙ y ∈ C ↔ ∀ y y ∈ ⦋ A / x⦌ B ↔ y ∈ ⦋ A / x⦌ C
15 6 8 14 3bitrd ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ∀ y y ∈ ⦋ A / x⦌ B ↔ y ∈ ⦋ A / x⦌ C
16 dfcleq ⊢ ⦋ A / x⦌ B = ⦋ A / x⦌ C ↔ ∀ y y ∈ ⦋ A / x⦌ B ↔ y ∈ ⦋ A / x⦌ C
17 15 16 bitr4di ⊢ A ∈ V → [˙A / x]˙ B = C ↔ ⦋ A / x⦌ B = ⦋ A / x⦌ C