Step |
Hyp |
Ref |
Expression |
1 |
|
raaan2.1 |
|- F/ y ph |
2 |
|
raaan2.2 |
|- F/ x ps |
3 |
|
dfbi3 |
|- ( ( A = (/) <-> B = (/) ) <-> ( ( A = (/) /\ B = (/) ) \/ ( -. A = (/) /\ -. B = (/) ) ) ) |
4 |
|
rzal |
|- ( A = (/) -> A. x e. A A. y e. B ( ph /\ ps ) ) |
5 |
4
|
adantr |
|- ( ( A = (/) /\ B = (/) ) -> A. x e. A A. y e. B ( ph /\ ps ) ) |
6 |
|
rzal |
|- ( A = (/) -> A. x e. A ph ) |
7 |
6
|
adantr |
|- ( ( A = (/) /\ B = (/) ) -> A. x e. A ph ) |
8 |
|
rzal |
|- ( B = (/) -> A. y e. B ps ) |
9 |
8
|
adantl |
|- ( ( A = (/) /\ B = (/) ) -> A. y e. B ps ) |
10 |
|
pm5.1 |
|- ( ( A. x e. A A. y e. B ( ph /\ ps ) /\ ( A. x e. A ph /\ A. y e. B ps ) ) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) ) |
11 |
5 7 9 10
|
syl12anc |
|- ( ( A = (/) /\ B = (/) ) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) ) |
12 |
|
df-ne |
|- ( B =/= (/) <-> -. B = (/) ) |
13 |
1
|
r19.28z |
|- ( B =/= (/) -> ( A. y e. B ( ph /\ ps ) <-> ( ph /\ A. y e. B ps ) ) ) |
14 |
13
|
ralbidv |
|- ( B =/= (/) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> A. x e. A ( ph /\ A. y e. B ps ) ) ) |
15 |
12 14
|
sylbir |
|- ( -. B = (/) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> A. x e. A ( ph /\ A. y e. B ps ) ) ) |
16 |
|
df-ne |
|- ( A =/= (/) <-> -. A = (/) ) |
17 |
|
nfcv |
|- F/_ x B |
18 |
17 2
|
nfralw |
|- F/ x A. y e. B ps |
19 |
18
|
r19.27z |
|- ( A =/= (/) -> ( A. x e. A ( ph /\ A. y e. B ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) ) |
20 |
16 19
|
sylbir |
|- ( -. A = (/) -> ( A. x e. A ( ph /\ A. y e. B ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) ) |
21 |
15 20
|
sylan9bbr |
|- ( ( -. A = (/) /\ -. B = (/) ) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) ) |
22 |
11 21
|
jaoi |
|- ( ( ( A = (/) /\ B = (/) ) \/ ( -. A = (/) /\ -. B = (/) ) ) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) ) |
23 |
3 22
|
sylbi |
|- ( ( A = (/) <-> B = (/) ) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) ) |