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