hboprab2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem hboprab2 3989

Description: The abstraction variables in an operation class abstraction are not free.

**Assertion**
Ref	Expression
hboprab2

**Proof of Theorem hboprab2**
Step	Hyp	Ref	Expression
1		df-oprab 3961	. 2 $/\$
2		hbe1 1015	. . . 4 $/\$ $/\$
3	2	hbex 1005	. . 3 $/\$ $/\$
4	3	hbab 1466	. 2 $/\$ $/\$
5	1, 4	hbxfr 1561	1

Colors of variables: wff set class

Syntax hints:

wi 3 $/\$ wa 223

wal 953

wceq 955

wcel 957

wex 979

cab 1462

cop 2408

This theorem is referenced by: elrnoprabg 4117 mapxpen 4484

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 961 ax-gen 962 ax-8 963 ax-10 965 ax-12 967 ax-17 970 ax-4 972 ax-5o 974 ax-6o 977 ax-9o 1122 ax-10o 1139 ax-16 1209 ax-11o 1217 ax-ext 1458

This theorem depends on definitions: df-bi 147 df-an 225 df-ex 980 df-sb 1171 df-clab 1463 df-cleq 1468 df-clel 1471 df-oprab 3961