Step |
Hyp |
Ref |
Expression |
1 |
|
solin |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B [C.] C \/ B = C \/ C [C.] B ) ) |
2 |
|
elex |
|- ( C e. A -> C e. _V ) |
3 |
2
|
ad2antll |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> C e. _V ) |
4 |
|
brrpssg |
|- ( C e. _V -> ( B [C.] C <-> B C. C ) ) |
5 |
3 4
|
syl |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B [C.] C <-> B C. C ) ) |
6 |
|
biidd |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B = C <-> B = C ) ) |
7 |
|
elex |
|- ( B e. A -> B e. _V ) |
8 |
7
|
ad2antrl |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> B e. _V ) |
9 |
|
brrpssg |
|- ( B e. _V -> ( C [C.] B <-> C C. B ) ) |
10 |
8 9
|
syl |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( C [C.] B <-> C C. B ) ) |
11 |
5 6 10
|
3orbi123d |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( ( B [C.] C \/ B = C \/ C [C.] B ) <-> ( B C. C \/ B = C \/ C C. B ) ) ) |
12 |
1 11
|
mpbid |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C. C \/ B = C \/ C C. B ) ) |
13 |
|
sspsstri |
|- ( ( B C_ C \/ C C_ B ) <-> ( B C. C \/ B = C \/ C C. B ) ) |
14 |
12 13
|
sylibr |
|- ( ( [C.] Or A /\ ( B e. A /\ C e. A ) ) -> ( B C_ C \/ C C_ B ) ) |