Description: Obsolete version of ineq1 as of 20-Sep-2023. Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ineq1OLD | |- ( A = B -> ( A i^i C ) = ( B i^i C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 | |- ( A = B -> ( x e. A <-> x e. B ) ) |
|
2 | 1 | anbi1d | |- ( A = B -> ( ( x e. A /\ x e. C ) <-> ( x e. B /\ x e. C ) ) ) |
3 | elin | |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) ) |
|
4 | elin | |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) ) |
|
5 | 2 3 4 | 3bitr4g | |- ( A = B -> ( x e. ( A i^i C ) <-> x e. ( B i^i C ) ) ) |
6 | 5 | eqrdv | |- ( A = B -> ( A i^i C ) = ( B i^i C ) ) |