ssoprab2i - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem ssoprab2i 4008

Description: Inference of operation class abstraction subclass from implication.

**Hypothesis**
Ref	Expression
ssoprab2i.1

**Assertion**
Ref	Expression
ssoprab2i

**Proof of Theorem ssoprab2i**
Step	Hyp	Ref	Expression
1		ssoprab2i.1	. . . . 5
2	1	anim2i 335	. . . 4 $/\$ $/\$
3	2	19.22i2 1041	. . 3 $/\$ $/\$
4	3	ssopab2i 2823	. 2 $/\$ $/\$
5		dfoprab2 3991	. 2 $/\$
6		dfoprab2 3991	. 2 $/\$
7	4, 5, 6	3sstr4 2100	1

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wceq 956

wex 980

wss 2047

cop 2411

copab 2666

This theorem is referenced by: blfval 7835 nvvcop 8213

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-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-opab 2667 df-oprab 3966