Theorem ssrel2 4373

Description: A subclass relationship depends only on a relation's ordered pairs. This version of ssrel 4371 is restricted to the relation's domain. (Contributed by Thierry Arnoux, 25-Jan-2018.)

Assertion

Ref	Expression
ssrel2	|- ( R C_ (A X. B) -> ( R C_ S <-> A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S)))

Distinct variable groups:   x,y,A   x,B,y   x, R,y   x, S,y

Proof of Theorem ssrel2

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 2933	. . . 4 |- ( R C_ S -> ( <.x , y >. e. R -> <.x , y >. e. S))
2	1	a1d 22	. . 3 |- ( R C_ S -> ((x e. A /\ y e. B) -> ( <.x , y >. e. R -> <.x , y >. e. S)))
3	2	ralrimivv 2394	. 2 |- ( R C_ S -> A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S))
4		eleq1 2097	. . . . . . . . . . . 12 |- (z = <.x , y >. -> (z e. R <-> <.x , y >. e. R))
5		eleq1 2097	. . . . . . . . . . . 12 |- (z = <.x , y >. -> (z e. S <-> <.x , y >. e. S))
6	4, 5	imbi12d 223	. . . . . . . . . . 11 |- (z = <.x , y >. -> ((z e. R -> z e. S) <-> ( <.x , y >. e. R -> <.x , y >. e. S)))
7	6	biimprcd 149	. . . . . . . . . 10 |- (( <.x , y >. e. R -> <.x , y >. e. S) -> (z = <.x , y >. -> (z e. R -> z e. S)))
8	7	ralimi 2378	. . . . . . . . 9 |- (A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> A.y e. B (z = <.x , y >. -> (z e. R -> z e. S)))
9	8	ralimi 2378	. . . . . . . 8 |- (A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> A.x e. A A.y e. B (z = <.x , y >. -> (z e. R -> z e. S)))
10		r19.23v 2419	. . . . . . . . . 10 |- (A.y e. B (z = <.x , y >. -> (z e. R -> z e. S)) <-> (E.y e. B z = <.x , y >. -> (z e. R -> z e. S)))
11	10	ralbii 2324	. . . . . . . . 9 |- (A.x e. A A.y e. B (z = <.x , y >. -> (z e. R -> z e. S)) <-> A.x e. A (E.y e. B z = <.x , y >. -> (z e. R -> z e. S)))
12		r19.23v 2419	. . . . . . . . 9 |- (A.x e. A (E.y e. B z = <.x , y >. -> (z e. R -> z e. S)) <-> (E.x e. A E.y e. B z = <.x , y >. -> (z e. R -> z e. S)))
13	11, 12	bitri 173	. . . . . . . 8 |- (A.x e. A A.y e. B (z = <.x , y >. -> (z e. R -> z e. S)) <-> (E.x e. A E.y e. B z = <.x , y >. -> (z e. R -> z e. S)))
14	9, 13	sylib 127	. . . . . . 7 |- (A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> (E.x e. A E.y e. B z = <.x , y >. -> (z e. R -> z e. S)))
15	14	com23 72	. . . . . 6 |- (A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> (z e. R -> (E.x e. A E.y e. B z = <.x , y >. -> z e. S)))
16	15	a2d 23	. . . . 5 |- (A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> ((z e. R -> E.x e. A E.y e. B z = <.x , y >.) -> (z e. R -> z e. S)))
17	16	alimdv 1756	. . . 4 |- (A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> (A.z(z e. R -> E.x e. A E.y e. B z = <.x , y >.) -> A.z(z e. R -> z e. S)))
18		dfss2 2928	. . . . 5 |- ( R C_ (A X. B) <-> A.z(z e. R -> z e. (A X. B)))
19		elxp2 4306	. . . . . . 7 |- (z e. (A X. B) <-> E.x e. A E.y e. B z = <.x , y >.)
20	19	imbi2i 215	. . . . . 6 |- ((z e. R -> z e. (A X. B)) <-> (z e. R -> E.x e. A E.y e. B z = <.x , y >.))
21	20	albii 1356	. . . . 5 |- (A.z(z e. R -> z e. (A X. B)) <-> A.z(z e. R -> E.x e. A E.y e. B z = <.x , y >.))
22	18, 21	bitri 173	. . . 4 |- ( R C_ (A X. B) <-> A.z(z e. R -> E.x e. A E.y e. B z = <.x , y >.))
23		dfss2 2928	. . . 4 |- ( R C_ S <-> A.z(z e. R -> z e. S))
24	17, 22, 23	3imtr4g 194	. . 3 |- (A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> ( R C_ (A X. B) -> R C_ S))
25	24	com12 27	. 2 |- ( R C_ (A X. B) -> (A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S) -> R C_ S))
26	3, 25	impbid2 131	1 |- ( R C_ (A X. B) -> ( R C_ S <-> A.x e. A A.y e. B ( <.x , y >. e. R -> <.x , y >. e. S)))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98  A.wal 1240   = wceq 1242   e. wcel 1390  A.wral 2300  E.wrex 2301   C_ wss 2911   <.cop 3370   X. cxp 4286

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-opab 3810  df-xp 4294

This theorem is referenced by: (None)