Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem ssoprab2i 3036

Description: Inference of operation abstraction subclass from implication.

**Hypothesis**
Ref	Expression
ssoprab2i.1

**Assertion**
Ref	Expression
ssoprab2i

Distinct variable group(s):

**Proof of Theorem ssoprab2i**
Step	Hyp	Ref	Expression
1		ssoprab2i.1	. . . . . 6
2	1	anim2i 270	. . . . 5 $/\$ $/\$
3	2	19.22i 723	. . . 4 $/\$ $/\$
4	3	19.22i 723	. . 3 $/\$ $/\$
5	4	ssopab2i 2120	. 2 $/\$ $/\$
6		dfoprab2 3021	. 2 $/\$
7		dfoprab2 3021	. 2 $/\$
8	5, 6, 7	3sstr4 1539	1

Colors of variables: wff set class

Syntax hints:

wi 2 $/\$ wa 196

wex 678

wceq 1091

wss 1487

cop 1810

copab 2055

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-ex 679 df-sb 853 df-clab 1093 df-cleq 1097 df-clel 1099 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-op 1815 df-opab 2098 df-oprab 3004