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