This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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