Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
Set theory
Complements on direct products
bj-cleq
Next ⟩
"Singletonization" and tagging
Metamath Proof Explorer
Ascii
Unicode
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