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 A B A B = A

Proof

Step Hyp Ref Expression
1 dfcleq y | y A y B = A x x y | y A y B x A
2 df-in A B = y | y A y B
3 2 eqeq1i A B = A y | y A y B = A
4 df-ss A B x x A x B
5 simp2 x A x B x A x B x A
6 5 3expib x A x B x A x B x A
7 ancl x A x B x A x A x B
8 6 7 impbid x A x B x A x B x A
9 dfbi2 x A x B x A x A x B x A x A x A x B
10 pm2.21 ¬ x A x A x B
11 pm3.4 x A x B x A x B
12 10 11 ja x A x A x B x A x B
13 9 12 simplbiim x A x B x A x A x B
14 8 13 impbii x A x B x A x B x A
15 df-clab x y | y A y B x y y A y B
16 eleq1w y = x y A x A
17 eleq1w y = x y B x B
18 16 17 anbi12d y = x y A y B x A x B
19 18 sbievw x y y A y B x A x B
20 15 19 bitr2i x A x B x y | y A y B
21 20 bibi1i x A x B x A x y | y A y B x A
22 14 21 bitri x A x B x y | y A y B x A
23 22 albii x x A x B x x y | y A y B x A
24 4 23 bitri A B x x y | y A y B x A
25 1 3 24 3bitr4ri A B A B = A