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.

Step	Hyp	Ref	Expression
1		ssel 3428	. . . . . 6 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 568	. . . . 5 |- ( A C_ B -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. C ) ) )
3	2	alrimiv 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 ) ) )
5	3, 4	syl 17	. . 3 |- ( A C_ B -> ( E* x ( x e. B /\ y e. C ) -> E* x ( x e. A /\ y e. C ) ) )
6	5	alimdv 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 ) )
9	6, 7, 8	3imtr4g 274	1 |- ( A C_ B -> (Disj x e. B C -> Disj x e. A C ) )

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