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