MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  disjss1 Structured version   Visualization version   Unicode version

Theorem disjss1 4382
Description: A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.)
Assertion
Ref Expression
disjss1  |-  ( A 
C_  B  ->  (Disj  x  e.  B  C  -> Disj  x  e.  A  C ) )
Distinct variable groups:    x, A    x, B
Allowed substitution hint:    C( x)

Proof of Theorem disjss1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 ssel 3428 . . . . . 6  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 568 . . . . 5  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  y  e.  C
)  ->  ( x  e.  B  /\  y  e.  C ) ) )
32alrimiv 1775 . . . 4  |-  ( A 
C_  B  ->  A. x
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  C )
) )
4 moim 2350 . . . 4  |-  ( A. x ( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  C )
)  ->  ( E* x ( x  e.  B  /\  y  e.  C )  ->  E* x ( x  e.  A  /\  y  e.  C ) ) )
53, 4syl 17 . . 3  |-  ( A 
C_  B  ->  ( E* x ( x  e.  B  /\  y  e.  C )  ->  E* x ( x  e.  A  /\  y  e.  C ) ) )
65alimdv 1765 . 2  |-  ( A 
C_  B  ->  ( A. y E* x ( x  e.  B  /\  y  e.  C )  ->  A. y E* x
( x  e.  A  /\  y  e.  C
) ) )
7 dfdisj2 4378 . 2  |-  (Disj  x  e.  B  C  <->  A. y E* x ( x  e.  B  /\  y  e.  C ) )
8 dfdisj2 4378 . 2  |-  (Disj  x  e.  A  C  <->  A. y E* x ( x  e.  A  /\  y  e.  C ) )
96, 7, 83imtr4g 274 1  |-  ( A 
C_  B  ->  (Disj  x  e.  B  C  -> Disj  x  e.  A  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   A.wal 1444    e. wcel 1889   E*wmo 2302    C_ wss 3406  Disj wdisj 4376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-rmo 2747  df-in 3413  df-ss 3420  df-disj 4377
This theorem is referenced by:  disjeq1  4383  disjx0  4400  disjxiun  4402  disjss3  4404  volfiniun  22512  uniioovol  22548  uniioombllem4  22556  disjiunel  28218  carsggect  29162  carsgclctunlem2  29163  omsmeas  29167  omsmeasOLD  29168  sibfof  29185  disjf1o  37476  fsumiunss  37664  sge0iunmptlemre  38267  meadjiunlem  38313
  Copyright terms: Public domain W3C validator