Theorem ssrin 2205

Description: Add right intersection to subclass relation.

Assertion

Ref	Expression
ssrin	|- (A (_ B -> (A i^i C) (_ (B i^i C))

Proof of Theorem ssrin

Step	Hyp	Ref	Expression
1		pm3.45 560	. . . 4 |- ((x e. A -> x e. B) -> ((x e. A /\ x e. C) -> (x e. B /\ x e. C)))
2		elin 2178	. . . 4 |- (x e. (A i^i C) <-> (x e. A /\ x e. C))
3		elin 2178	. . . 4 |- (x e. (B i^i C) <-> (x e. B /\ x e. C))
4	1, 2, 3	3imtr4g 551	. . 3 |- ((x e. A -> x e. B) -> (x e. (A i^i C) -> x e. (B i^i C)))
5	4	19.20i 968	. 2 |- (A.x(x e. A -> x e. B) -> A.x(x e. (A i^i C) -> x e. (B i^i C)))
6		dfss2 2029	. 2 |- (A (_ B <-> A.x(x e. A -> x e. B))
7		dfss2 2029	. 2 |- ((A i^i C) (_ (B i^i C) <-> A.x(x e. (A i^i C) -> x e. (B i^i C)))
8	5, 6, 7	3imtr4 219	1 |- (A (_ B -> (A i^i C) (_ (B i^i C))

Syntax hints:   -> wi 3   /\ wa 223  A.wal 950   e. wcel 1105   i^i cin 2017   (_ wss 2018

This theorem is referenced by:  sslin 2206  ss2in 2207  ssdisj 2289  ssres 3336  sbthlem7 4387  phplem2 4441  tgsst 7529  islp2 7636  orthin 9499  3oalem6 9743  mdbr2 10347  mdslle1 10366  mdslle2 10367  mdslj1 10368  mdslj2 10369  mdsl2 10371  mdslmd1lem1 10374  mdslmd1lem2 10375  mdslmd3 10381  mdexch 10384  sumdmdlem 10466

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787  df-in 2022  df-ss 2024

Copyright terms: Public domain