Theorem dfss2

Description: Alternate definition of the subclass relationship between two classes. Definition 5.9 of TakeutiZaring p. 17. (Contributed by NM, 8-Jan-2002)

	Ref	Expression
Assertion	dfss2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dfss	⊢ ( 𝐴 ⊆ 𝐵 ↔ 𝐴 = ( 𝐴 ∩ 𝐵 ) )
2		df-in	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) }
3	2	eqeq2i	⊢ ( 𝐴 = ( 𝐴 ∩ 𝐵 ) ↔ 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } )
4		abeq2	⊢ ( 𝐴 = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
5	1 3 4	3bitri	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
6		pm4.71	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
7	6	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
8	5 7	bitr4i	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )