Step |
Hyp |
Ref |
Expression |
1 |
|
onint |
|- ( ( B C_ On /\ B =/= (/) ) -> |^| B e. B ) |
2 |
|
eleq1 |
|- ( A = |^| B -> ( A e. B <-> |^| B e. B ) ) |
3 |
1 2
|
syl5ibrcom |
|- ( ( B C_ On /\ B =/= (/) ) -> ( A = |^| B -> A e. B ) ) |
4 |
|
eleq2 |
|- ( A = |^| B -> ( x e. A <-> x e. |^| B ) ) |
5 |
4
|
biimpd |
|- ( A = |^| B -> ( x e. A -> x e. |^| B ) ) |
6 |
|
onnmin |
|- ( ( B C_ On /\ x e. B ) -> -. x e. |^| B ) |
7 |
6
|
ex |
|- ( B C_ On -> ( x e. B -> -. x e. |^| B ) ) |
8 |
7
|
con2d |
|- ( B C_ On -> ( x e. |^| B -> -. x e. B ) ) |
9 |
5 8
|
syl9r |
|- ( B C_ On -> ( A = |^| B -> ( x e. A -> -. x e. B ) ) ) |
10 |
9
|
ralrimdv |
|- ( B C_ On -> ( A = |^| B -> A. x e. A -. x e. B ) ) |
11 |
10
|
adantr |
|- ( ( B C_ On /\ B =/= (/) ) -> ( A = |^| B -> A. x e. A -. x e. B ) ) |
12 |
3 11
|
jcad |
|- ( ( B C_ On /\ B =/= (/) ) -> ( A = |^| B -> ( A e. B /\ A. x e. A -. x e. B ) ) ) |
13 |
|
oneqmini |
|- ( B C_ On -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) ) |
14 |
13
|
adantr |
|- ( ( B C_ On /\ B =/= (/) ) -> ( ( A e. B /\ A. x e. A -. x e. B ) -> A = |^| B ) ) |
15 |
12 14
|
impbid |
|- ( ( B C_ On /\ B =/= (/) ) -> ( A = |^| B <-> ( A e. B /\ A. x e. A -. x e. B ) ) ) |