Theorem ssel

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	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )

Proof

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	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 ) )