**Description:** Membership relationships follow from a subclass relationship.
(Contributed by NM, 5-Aug-1993) Avoid ax-12 . (Revised by SN, 27-May-2024)

Ref | Expression | ||
---|---|---|---|

Assertion | ssel | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | dfss2 | ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) | |

2 | id | ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) | |

3 | 2 | anim2d | ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) ) |

4 | 3 | aleximi | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) ) |

5 | dfclel | ⊢ ( 𝐶 ∈ 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐴 ) ) | |

6 | dfclel | ⊢ ( 𝐶 ∈ 𝐵 ↔ ∃ 𝑥 ( 𝑥 = 𝐶 ∧ 𝑥 ∈ 𝐵 ) ) | |

7 | 4 5 6 | 3imtr4g | ⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) ) |

8 | 1 7 | sylbi | ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) ) |