oprabss - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem oprabss 4006

Description: Structure of an operation class abstraction.

**Assertion**
Ref	Expression
oprabss

**Proof of Theorem oprabss**
Step	Hyp	Ref	Expression
1		reloprab 3992	. . 3
2		relssdr 3513	. . 3
3	1, 2	ax-mp 7	. 2
4		reldmoprab 4005	. . . 4
5		df-rel 3185	. . . 4
6	4, 5	mpbi 189	. . 3
7		ssv 2081	. . 3
8		ssxp 3256	. . 3 $/\$
9	6, 7, 8	mp2an 697	. 2
10	3, 9	sstri 2073	1

Colors of variables: wff set class

Syntax hints:

cvv 1811

wss 2047

cxp 3168

cdm 3170

crn 3171

wrel 3175

This theorem is referenced by: nvss 8212

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-9 965 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-sep 2703 ax-pow 2742 ax-pr 2779

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-v 1812 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-nul 2281 df-pw 2402 df-sn 2412 df-pr 2413 df-op 2416 df-br 2620 df-opab 2667 df-xp 3184 df-rel 3185 df-cnv 3186 df-dm 3188 df-rn 3189 df-oprab 3966