oprabss - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem oprabss 4001

Description: Structure of an operation class abstraction.

**Assertion**
Ref	Expression
oprabss

**Proof of Theorem oprabss**
Step	Hyp	Ref	Expression
1		reloprab 3987	. . 3
2		relssdr 3509	. . 3
3	1, 2	ax-mp 7	. 2
4		reldmoprab 4000	. . . 4
5		df-rel 3181	. . . 4
6	4, 5	mpbi 189	. . 3
7		ssv 2078	. . 3
8		ssxp 3252	. . 3 $/\$
9	6, 7, 8	mp2an 696	. 2
10	3, 9	sstri 2070	1

Colors of variables: wff set class

Syntax hints:

cvv 1808

wss 2044

cxp 3164

cdm 3166

crn 3167

wrel 3171

This theorem is referenced by: nvss 8176

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 961 ax-gen 962 ax-8 963 ax-9 964 ax-10 965 ax-11 966 ax-12 967 ax-13 968 ax-14 969 ax-17 970 ax-4 972 ax-5o 974 ax-6o 977 ax-9o 1122 ax-10o 1139 ax-16 1209 ax-11o 1217 ax-ext 1458 ax-sep 2699 ax-pow 2738 ax-pr 2775

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 980 df-sb 1171 df-eu 1381 df-mo 1382 df-clab 1463 df-cleq 1468 df-clel 1471 df-ne 1585 df-v 1809 df-dif 2046 df-un 2047 df-in 2048 df-ss 2050 df-nul 2278 df-pw 2399 df-sn 2409 df-pr 2410 df-op 2413 df-br 2616 df-opab 2663 df-xp 3180 df-rel 3181 df-cnv 3182 df-dm 3184 df-rn 3185 df-oprab 3961