Metamath Proof Explorer


Theorem bj-cleq

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

Ref Expression
Assertion bj-cleq ( 𝐴 = 𝐵 → { 𝑥 ∣ { 𝑥 } ∈ ( 𝐴𝐶 ) } = { 𝑥 ∣ { 𝑥 } ∈ ( 𝐵𝐶 ) } )

Proof

Step Hyp Ref Expression
1 imaeq1 ( 𝐴 = 𝐵 → ( 𝐴𝐶 ) = ( 𝐵𝐶 ) )
2 eleq2 ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) → ( { 𝑥 } ∈ ( 𝐴𝐶 ) ↔ { 𝑥 } ∈ ( 𝐵𝐶 ) ) )
3 2 alrimiv ( ( 𝐴𝐶 ) = ( 𝐵𝐶 ) → ∀ 𝑥 ( { 𝑥 } ∈ ( 𝐴𝐶 ) ↔ { 𝑥 } ∈ ( 𝐵𝐶 ) ) )
4 abbi1 ( ∀ 𝑥 ( { 𝑥 } ∈ ( 𝐴𝐶 ) ↔ { 𝑥 } ∈ ( 𝐵𝐶 ) ) → { 𝑥 ∣ { 𝑥 } ∈ ( 𝐴𝐶 ) } = { 𝑥 ∣ { 𝑥 } ∈ ( 𝐵𝐶 ) } )
5 1 3 4 3syl ( 𝐴 = 𝐵 → { 𝑥 ∣ { 𝑥 } ∈ ( 𝐴𝐶 ) } = { 𝑥 ∣ { 𝑥 } ∈ ( 𝐵𝐶 ) } )