ssoprab2i - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem ssoprab2i 3993

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 1037	. . 3 $/\$ $/\$
4	3	ssopab2i 2812	. 2 $/\$ $/\$
5		dfoprab2 3976	. 2 $/\$
6		dfoprab2 3976	. 2 $/\$
7	4, 5, 6	3sstr4 2090	1

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wceq 953

wex 977

wss 2037

cop 2401

copab 2656

This theorem is referenced by: blfval 7775 nvvcop 8151

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-sep 2693 ax-pow 2732 ax-pr 2769

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-nul 2271 df-pw 2392 df-sn 2402 df-pr 2403 df-op 2406 df-opab 2657 df-oprab 3951