This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐴 )