Theorem dfss2

Description: Alternate definition of the subclass relationship between two classes. Exercise 9 of TakeutiZaring p. 18. This was the original definition before df-ss . (Contributed by NM, 27-Apr-1994) Revise df-ss . (Revised by GG, 15-May-2025)

	Ref	Expression
Assertion	dfss2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } = 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ↔ 𝑥 ∈ 𝐴 ) )
2		df-in	⊢ ( 𝐴 ∩ 𝐵 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) }
3	2	eqeq1i	⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐴 ↔ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } = 𝐴 )
4		df-ss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
5		simp2	⊢ ( ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
6	5	3expib	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 ) )
7		ancl	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
8	6 7	impbid	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) )
9		dfbi2	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) ) )
10		pm2.21	⊢ ( ¬ 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
11		pm3.4	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
12	10 11	ja	⊢ ( ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
13	9 12	simplbiim	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
14	8 13	impbii	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) )
15		df-clab	⊢ ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ↔ [ 𝑥 / 𝑦 ] ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
16		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
17		eleq1w	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ 𝐵 ↔ 𝑥 ∈ 𝐵 ) )
18	16 17	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ) )
19	18	sbievw	⊢ ( [ 𝑥 / 𝑦 ] ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) )
20	15 19	bitr2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } )
21	20	bibi1i	⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵 ) ↔ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ↔ 𝑥 ∈ 𝐴 ) )
22	14 21	bitri	⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ↔ 𝑥 ∈ 𝐴 ) )
23	22	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ↔ 𝑥 ∈ 𝐴 ) )
24	4 23	bitri	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑦 ∣ ( 𝑦 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) } ↔ 𝑥 ∈ 𝐴 ) )
25	1 3 24	3bitr4ri	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )