Description: Obsolete version of ssel as of 27-May-2024. (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | sselOLD | |- ( A C_ B -> ( C e. A -> C e. B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfss2 | |- ( A C_ B <-> A. x ( x e. A -> x e. B ) ) |
|
| 2 | 1 | biimpi | |- ( A C_ B -> A. x ( x e. A -> x e. B ) ) |
| 3 | 2 | 19.21bi | |- ( A C_ B -> ( x e. A -> x e. B ) ) |
| 4 | 3 | anim2d | |- ( A C_ B -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) ) |
| 5 | 4 | eximdv | |- ( A C_ B -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) ) |
| 6 | dfclel | |- ( C e. A <-> E. x ( x = C /\ x e. A ) ) |
|
| 7 | dfclel | |- ( C e. B <-> E. x ( x = C /\ x e. B ) ) |
|
| 8 | 5 6 7 | 3imtr4g | |- ( A C_ B -> ( C e. A -> C e. B ) ) |