Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem hboprab1 3023

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

**Assertion**
Ref	Expression
hboprab1

Distinct variable group(s):

**Proof of Theorem hboprab1**
Step	Hyp	Ref	Expression
1		hbe1 709	. . 3 $/\$ $/\$
2	1	hbab 1096	. 2 $/\$ $/\$
3		df-oprab 3004	. . 3 $/\$
4	3	eleq2i 1153	. 2 $/\$
5	4	bial 695	. 2 $/\$
6	2, 4, 5	3imtr4 192	1

Colors of variables: wff set class

Syntax hints:

wi 2 $/\$ wa 196

wal 672

wex 678

cab 1090

wceq 1091

wcel 1092

cop 1810

This theorem is referenced by: elrnoprab 3054 mapxpen 3390

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-16 922 ax-17 925 ax-ext 1074

This theorem depends on definitions: df-bi 128 df-an 198 df-ex 679 df-sb 853 df-clab 1093 df-cleq 1097 df-clel 1099 df-oprab 3004