Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  raaan2 Unicode version

Theorem raaan2 28056
Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 3574. It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
Hypotheses
Ref Expression
raaan2.1  |-  F/ y
ph
raaan2.2  |-  F/ x ps
Assertion
Ref Expression
raaan2  |-  ( ( A  =  (/)  <->  B  =  (/) )  ->  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. y  e.  B  ps ) ) )
Distinct variable groups:    x, y, A    x, B, y
Allowed substitution hints:    ph( x, y)    ps( x, y)

Proof of Theorem raaan2
StepHypRef Expression
1 dfbi3 863 . 2  |-  ( ( A  =  (/)  <->  B  =  (/) )  <->  ( ( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) ) )
2 rzal 3568 . . . . 5  |-  ( A  =  (/)  ->  A. x  e.  A  A. y  e.  B  ( ph  /\ 
ps ) )
32adantr 451 . . . 4  |-  ( ( A  =  (/)  /\  B  =  (/) )  ->  A. x  e.  A  A. y  e.  B  ( ph  /\ 
ps ) )
4 rzal 3568 . . . . 5  |-  ( A  =  (/)  ->  A. x  e.  A  ph )
54adantr 451 . . . 4  |-  ( ( A  =  (/)  /\  B  =  (/) )  ->  A. x  e.  A  ph )
6 rzal 3568 . . . . 5  |-  ( B  =  (/)  ->  A. y  e.  B  ps )
76adantl 452 . . . 4  |-  ( ( A  =  (/)  /\  B  =  (/) )  ->  A. y  e.  B  ps )
8 pm5.1 830 . . . 4  |-  ( ( 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 ) ) )
93, 5, 7, 8syl12anc 1180 . . 3  |-  ( ( A  =  (/)  /\  B  =  (/) )  ->  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  ( A. x  e.  A  ph 
/\  A. y  e.  B  ps ) ) )
10 df-ne 2461 . . . . 5  |-  ( B  =/=  (/)  <->  -.  B  =  (/) )
11 raaan2.1 . . . . . . 7  |-  F/ y
ph
1211r19.28z 3559 . . . . . 6  |-  ( B  =/=  (/)  ->  ( A. y  e.  B  ( ph  /\  ps )  <->  ( ph  /\ 
A. y  e.  B  ps ) ) )
1312ralbidv 2576 . . . . 5  |-  ( B  =/=  (/)  ->  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  A. x  e.  A  ( ph  /\ 
A. y  e.  B  ps ) ) )
1410, 13sylbir 204 . . . 4  |-  ( -.  B  =  (/)  ->  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  A. x  e.  A  (
ph  /\  A. y  e.  B  ps )
) )
15 df-ne 2461 . . . . 5  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
16 nfcv 2432 . . . . . . 7  |-  F/_ x B
17 raaan2.2 . . . . . . 7  |-  F/ x ps
1816, 17nfral 2609 . . . . . 6  |-  F/ x A. y  e.  B  ps
1918r19.27z 3565 . . . . 5  |-  ( A  =/=  (/)  ->  ( A. x  e.  A  ( ph  /\  A. y  e.  B  ps )  <->  ( A. x  e.  A  ph  /\  A. y  e.  B  ps ) ) )
2015, 19sylbir 204 . . . 4  |-  ( -.  A  =  (/)  ->  ( A. x  e.  A  ( ph  /\  A. y  e.  B  ps )  <->  ( A. x  e.  A  ph 
/\  A. y  e.  B  ps ) ) )
2114, 20sylan9bbr 681 . . 3  |-  ( ( -.  A  =  (/)  /\ 
-.  B  =  (/) )  ->  ( A. x  e.  A  A. y  e.  B  ( ph  /\ 
ps )  <->  ( A. x  e.  A  ph  /\  A. y  e.  B  ps ) ) )
229, 21jaoi 368 . 2  |-  ( ( ( A  =  (/)  /\  B  =  (/) )  \/  ( -.  A  =  (/)  /\  -.  B  =  (/) ) )  ->  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  ( A. x  e.  A  ph 
/\  A. y  e.  B  ps ) ) )
231, 22sylbi 187 1  |-  ( ( A  =  (/)  <->  B  =  (/) )  ->  ( A. x  e.  A  A. y  e.  B  ( ph  /\  ps )  <->  ( A. x  e.  A  ph  /\  A. y  e.  B  ps ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358   F/wnf 1534    = wceq 1632    =/= wne 2459   A.wral 2556   (/)c0 3468
This theorem is referenced by:  2reu4a  28070
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator