Step |
Hyp |
Ref |
Expression |
1 |
|
rp-fakeanorass |
|- ( ( x e. C -> x e. A ) <-> ( ( ( x e. A /\ x e. B ) \/ x e. C ) <-> ( x e. A /\ ( x e. B \/ x e. C ) ) ) ) |
2 |
1
|
albii |
|- ( A. x ( x e. C -> x e. A ) <-> A. x ( ( ( x e. A /\ x e. B ) \/ x e. C ) <-> ( x e. A /\ ( x e. B \/ x e. C ) ) ) ) |
3 |
|
dfss2 |
|- ( C C_ A <-> A. x ( x e. C -> x e. A ) ) |
4 |
|
dfcleq |
|- ( ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) <-> A. x ( x e. ( ( A i^i B ) u. C ) <-> x e. ( A i^i ( B u. C ) ) ) ) |
5 |
|
elun |
|- ( x e. ( ( A i^i B ) u. C ) <-> ( x e. ( A i^i B ) \/ x e. C ) ) |
6 |
|
elin |
|- ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) ) |
7 |
6
|
orbi1i |
|- ( ( x e. ( A i^i B ) \/ x e. C ) <-> ( ( x e. A /\ x e. B ) \/ x e. C ) ) |
8 |
5 7
|
bitri |
|- ( x e. ( ( A i^i B ) u. C ) <-> ( ( x e. A /\ x e. B ) \/ x e. C ) ) |
9 |
|
elin |
|- ( x e. ( A i^i ( B u. C ) ) <-> ( x e. A /\ x e. ( B u. C ) ) ) |
10 |
|
elun |
|- ( x e. ( B u. C ) <-> ( x e. B \/ x e. C ) ) |
11 |
10
|
anbi2i |
|- ( ( x e. A /\ x e. ( B u. C ) ) <-> ( x e. A /\ ( x e. B \/ x e. C ) ) ) |
12 |
9 11
|
bitri |
|- ( x e. ( A i^i ( B u. C ) ) <-> ( x e. A /\ ( x e. B \/ x e. C ) ) ) |
13 |
8 12
|
bibi12i |
|- ( ( x e. ( ( A i^i B ) u. C ) <-> x e. ( A i^i ( B u. C ) ) ) <-> ( ( ( x e. A /\ x e. B ) \/ x e. C ) <-> ( x e. A /\ ( x e. B \/ x e. C ) ) ) ) |
14 |
13
|
albii |
|- ( A. x ( x e. ( ( A i^i B ) u. C ) <-> x e. ( A i^i ( B u. C ) ) ) <-> A. x ( ( ( x e. A /\ x e. B ) \/ x e. C ) <-> ( x e. A /\ ( x e. B \/ x e. C ) ) ) ) |
15 |
4 14
|
bitri |
|- ( ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) <-> A. x ( ( ( x e. A /\ x e. B ) \/ x e. C ) <-> ( x e. A /\ ( x e. B \/ x e. C ) ) ) ) |
16 |
2 3 15
|
3bitr4i |
|- ( C C_ A <-> ( ( A i^i B ) u. C ) = ( A i^i ( B u. C ) ) ) |