Metamath Proof Explorer


Theorem raaan2

Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan . It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017)

Ref Expression
Hypotheses raaan2.1
|- F/ y ph
raaan2.2
|- F/ x ps
Assertion raaan2
|- ( ( A = (/) <-> B = (/) ) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) )

Proof

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 ) ) )