Metamath Proof Explorer


Theorem ssrel2

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

Ref Expression
Assertion ssrel2 R A × B R S x A y B x y R x y S

Proof

Step Hyp Ref Expression
1 ssel R S x y R x y S
2 1 a1d R S x A y B x y R x y S
3 2 ralrimivv R S x A y B x y R x y S
4 eleq1 z = x y z R x y R
5 eleq1 z = x y z S x y S
6 4 5 imbi12d z = x y z R z S x y R x y S
7 6 biimprcd x y R x y S z = x y z R z S
8 7 2ralimi x A y B x y R x y S x A y B z = x y z R z S
9 r19.23v y B z = x y z R z S y B z = x y z R z S
10 9 ralbii x A y B z = x y z R z S x A y B z = x y z R z S
11 r19.23v x A y B z = x y z R z S x A y B z = x y z R z S
12 10 11 bitri x A y B z = x y z R z S x A y B z = x y z R z S
13 8 12 sylib x A y B x y R x y S x A y B z = x y z R z S
14 13 com23 x A y B x y R x y S z R x A y B z = x y z S
15 14 a2d x A y B x y R x y S z R x A y B z = x y z R z S
16 15 alimdv x A y B x y R x y S z z R x A y B z = x y z z R z S
17 dfss2 R A × B z z R z A × B
18 elxp2 z A × B x A y B z = x y
19 18 imbi2i z R z A × B z R x A y B z = x y
20 19 albii z z R z A × B z z R x A y B z = x y
21 17 20 bitri R A × B z z R x A y B z = x y
22 dfss2 R S z z R z S
23 16 21 22 3imtr4g x A y B x y R x y S R A × B R S
24 23 com12 R A × B x A y B x y R x y S R S
25 3 24 impbid2 R A × B R S x A y B x y R x y S