Metamath Proof Explorer

Theorem bj-cleq

Description: Substitution property for certain classes. (Contributed by BJ, 2-Apr-2019)

Ref Expression
Assertion bj-cleq ⊢ A = B → x | x ∈ A C = x | x ∈ B C

Proof

Step Hyp Ref Expression
1 imaeq1 ⊢ A = B → A C = B C
2 eleq2 ⊢ A C = B C → x ∈ A C ↔ x ∈ B C
3 2 alrimiv ⊢ A C = B C → ∀ x x ∈ A C ↔ x ∈ B C
4 abbi1 ⊢ ∀ x x ∈ A C ↔ x ∈ B C → x | x ∈ A C = x | x ∈ B C
5 1 3 4 3syl ⊢ A = B → x | x ∈ A C = x | x ∈ B C