oprabss - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem oprabss 4935

Description: Structure of an operation class abstraction.

**Assertion**
Ref	Expression
oprabss

**Proof of Theorem oprabss**
Step	Hyp	Ref	Expression
1		reloprab 4918	. . 3
2		relssdmrn 4416	. . 3
3	1, 2	ax-mp 7	. 2
4		reldmoprab 4934	. . . 4
5		df-rel 4001	. . . 4
6	4, 5	mpbi 206	. . 3
7		ssv 2636	. . 3
8		xpss12 4089	. . 3 $/\$
9	6, 7, 8	mp2an 761	. 2
10	3, 9	sstri 2626	1

Colors of variables: wff set class

Syntax hints:

cvv 2292

wss 2593

cxp 3984

cdm 3986

crn 3987

wrel 3991

This theorem is referenced by: nvss 9544

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-br 3339 df-opab 3396 df-xp 4000 df-rel 4001 df-cnv 4002 df-dm 4004 df-rn 4005 df-oprab 4887