Step |
Hyp |
Ref |
Expression |
1 |
|
elpri |
|- ( C e. { A , B } -> ( C = A \/ C = B ) ) |
2 |
|
eleq1 |
|- ( v = B -> ( v e. { A , B } <-> B e. { A , B } ) ) |
3 |
|
simprrr |
|- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. V ) |
4 |
|
necom |
|- ( A =/= B <-> B =/= A ) |
5 |
|
neeq2 |
|- ( A = C -> ( B =/= A <-> B =/= C ) ) |
6 |
5
|
eqcoms |
|- ( C = A -> ( B =/= A <-> B =/= C ) ) |
7 |
6
|
biimpcd |
|- ( B =/= A -> ( C = A -> B =/= C ) ) |
8 |
4 7
|
sylbi |
|- ( A =/= B -> ( C = A -> B =/= C ) ) |
9 |
8
|
adantr |
|- ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = A -> B =/= C ) ) |
10 |
9
|
impcom |
|- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B =/= C ) |
11 |
3 10
|
eldifsnd |
|- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. ( V \ { C } ) ) |
12 |
|
prid2g |
|- ( B e. V -> B e. { A , B } ) |
13 |
12
|
adantl |
|- ( ( A e. V /\ B e. V ) -> B e. { A , B } ) |
14 |
13
|
ad2antll |
|- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> B e. { A , B } ) |
15 |
2 11 14
|
rspcedvdw |
|- ( ( C = A /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) |
16 |
15
|
ex |
|- ( C = A -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) ) |
17 |
|
eleq1 |
|- ( v = A -> ( v e. { A , B } <-> A e. { A , B } ) ) |
18 |
|
simprrl |
|- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. V ) |
19 |
|
neeq2 |
|- ( B = C -> ( A =/= B <-> A =/= C ) ) |
20 |
19
|
eqcoms |
|- ( C = B -> ( A =/= B <-> A =/= C ) ) |
21 |
20
|
biimpcd |
|- ( A =/= B -> ( C = B -> A =/= C ) ) |
22 |
21
|
adantr |
|- ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> ( C = B -> A =/= C ) ) |
23 |
22
|
impcom |
|- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A =/= C ) |
24 |
18 23
|
eldifsnd |
|- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. ( V \ { C } ) ) |
25 |
|
prid1g |
|- ( A e. V -> A e. { A , B } ) |
26 |
25
|
adantr |
|- ( ( A e. V /\ B e. V ) -> A e. { A , B } ) |
27 |
26
|
ad2antll |
|- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> A e. { A , B } ) |
28 |
17 24 27
|
rspcedvdw |
|- ( ( C = B /\ ( A =/= B /\ ( A e. V /\ B e. V ) ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) |
29 |
28
|
ex |
|- ( C = B -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) ) |
30 |
16 29
|
jaoi |
|- ( ( C = A \/ C = B ) -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) ) |
31 |
1 30
|
syl |
|- ( C e. { A , B } -> ( ( A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) ) |
32 |
31
|
3impib |
|- ( ( C e. { A , B } /\ A =/= B /\ ( A e. V /\ B e. V ) ) -> E. v e. ( V \ { C } ) v e. { A , B } ) |