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 ) ) |