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

Theorem raaan2 27459
Description: Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 3650. 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 3644 . . . . 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 3644 . . . . 5  |-  ( A  =  (/)  ->  A. x  e.  A  ph )
54adantr 451 . . . 4  |-  ( ( A  =  (/)  /\  B  =  (/) )  ->  A. x  e.  A  ph )
6 rzal 3644 . . . . 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 1181 . . 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 2531 . . . . 5  |-  ( B  =/=  (/)  <->  -.  B  =  (/) )
11 raaan2.1 . . . . . . 7  |-  F/ y
ph
1211r19.28z 3635 . . . . . 6  |-  ( B  =/=  (/)  ->  ( A. y  e.  B  ( ph  /\  ps )  <->  ( ph  /\ 
A. y  e.  B  ps ) ) )
1312ralbidv 2648 . . . . 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 2531 . . . . 5  |-  ( A  =/=  (/)  <->  -.  A  =  (/) )
16 nfcv 2502 . . . . . . 7  |-  F/_ x B
17 raaan2.2 . . . . . . 7  |-  F/ x ps
1816, 17nfral 2681 . . . . . 6  |-  F/ x A. y  e.  B  ps
1918r19.27z 3641 . . . . 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 1549    = wceq 1647    =/= wne 2529   A.wral 2628   (/)c0 3543
This theorem is referenced by:  2reu4a  27473
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-nfc 2491  df-ne 2531  df-ral 2633  df-v 2875  df-dif 3241  df-nul 3544
  Copyright terms: Public domain W3C validator