df-dih - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-dih		Structured version Visualization version Unicode version

Definition df-dih 36518

Description: Define isomorphism H. (Contributed by NM, 28-Jan-2014.)

**Assertion**
Ref	Expression
df-dih	$/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-dih**
Step	Hyp	Ref	Expression
1		cdih 36517	. 2
2		vk	. . 3
3		cvv 3200	. . 3
4		vw	. . . 4
5	2	cv 1482	. . . . 5
6		clh 35270	. . . . 5
7	5, 6	cfv 5888	. . . 4
8		vx	. . . . 5
9		cbs 15857	. . . . . 6
10	5, 9	cfv 5888	. . . . 5
11	8	cv 1482	. . . . . . 7
12	4	cv 1482	. . . . . . 7
13		cple 15948	. . . . . . . 8
14	5, 13	cfv 5888	. . . . . . 7
15	11, 12, 14	wbr 4653	. . . . . 6
16		cdib 36427	. . . . . . . . 9
17	5, 16	cfv 5888	. . . . . . . 8
18	12, 17	cfv 5888	. . . . . . 7
19	11, 18	cfv 5888	. . . . . 6
20		vq	. . . . . . . . . . . . 13
21	20	cv 1482	. . . . . . . . . . . 12
22	21, 12, 14	wbr 4653	. . . . . . . . . . 11
23	22	wn 3	. . . . . . . . . 10
24		cmee 16945	. . . . . . . . . . . . . 14
25	5, 24	cfv 5888	. . . . . . . . . . . . 13
26	11, 12, 25	co 6650	. . . . . . . . . . . 12
27		cjn 16944	. . . . . . . . . . . . 13
28	5, 27	cfv 5888	. . . . . . . . . . . 12
29	21, 26, 28	co 6650	. . . . . . . . . . 11
30	29, 11	wceq 1483	. . . . . . . . . 10
31	23, 30	wa 384	. . . . . . . . 9 $/\$
32		vu	. . . . . . . . . . 11
33	32	cv 1482	. . . . . . . . . 10
34		cdic 36461	. . . . . . . . . . . . . 14
35	5, 34	cfv 5888	. . . . . . . . . . . . 13
36	12, 35	cfv 5888	. . . . . . . . . . . 12
37	21, 36	cfv 5888	. . . . . . . . . . 11
38	26, 18	cfv 5888	. . . . . . . . . . 11
39		cdvh 36367	. . . . . . . . . . . . . 14
40	5, 39	cfv 5888	. . . . . . . . . . . . 13
41	12, 40	cfv 5888	. . . . . . . . . . . 12
42		clsm 18049	. . . . . . . . . . . 12
43	41, 42	cfv 5888	. . . . . . . . . . 11
44	37, 38, 43	co 6650	. . . . . . . . . 10
45	33, 44	wceq 1483	. . . . . . . . 9
46	31, 45	wi 4	. . . . . . . 8 $/\$
47		catm 34550	. . . . . . . . 9
48	5, 47	cfv 5888	. . . . . . . 8
49	46, 20, 48	wral 2912	. . . . . . 7 $/\$
50		clss 18932	. . . . . . . 8
51	41, 50	cfv 5888	. . . . . . 7
52	49, 32, 51	crio 6610	. . . . . 6 $/\$
53	15, 19, 52	cif 4086	. . . . 5 $/\$
54	8, 10, 53	cmpt 4729	. . . 4 $/\$
55	4, 7, 54	cmpt 4729	. . 3 $/\$
56	2, 3, 55	cmpt 4729	. 2 $/\$
57	1, 56	wceq 1483	1 $/\$

Colors of variables: wff setvar class

This definition is referenced by: dihffval 36519

W3C validator