Theorem brfs 33930

Description: Binary relation form of the general five segment predicate. (Contributed by Scott Fenton, 5-Oct-2013.)

Assertion

Ref	Expression
brfs	⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ FiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝐺⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))

Proof of Theorem brfs

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 ℎ 𝑝 𝑞 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq1 5035	. . 3 ⊢ (𝑎 = 𝐴 → (𝑎 Colinear ⟨𝑏, 𝑐⟩ ↔ 𝐴 Colinear ⟨𝑏, 𝑐⟩))
2		opeq1 4761	. . . 4 ⊢ (𝑎 = 𝐴 → ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝑏, 𝑐⟩⟩)
3	2	breq1d 5042	. . 3 ⊢ (𝑎 = 𝐴 → (⟨𝑎, ⟨𝑏, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ↔ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩))
4		opeq1 4761	. . . . 5 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑑⟩ = ⟨𝐴, 𝑑⟩)
5	4	breq1d 5042	. . . 4 ⊢ (𝑎 = 𝐴 → (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩))
6	5	anbi1d 632	. . 3 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩)))
7	1, 3, 6	3anbi123d 1433	. 2 ⊢ (𝑎 = 𝐴 → ((𝑎 Colinear ⟨𝑏, 𝑐⟩ ∧ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝑏, 𝑐⟩ ∧ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩))))
8		opeq1 4761	. . . 4 ⊢ (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
9	8	breq2d 5044	. . 3 ⊢ (𝑏 = 𝐵 → (𝐴 Colinear ⟨𝑏, 𝑐⟩ ↔ 𝐴 Colinear ⟨𝐵, 𝑐⟩))
10	8	opeq2d 4770	. . . 4 ⊢ (𝑏 = 𝐵 → ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝑐⟩⟩)
11	10	breq1d 5042	. . 3 ⊢ (𝑏 = 𝐵 → (⟨𝐴, ⟨𝑏, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩))
12		opeq1 4761	. . . . 5 ⊢ (𝑏 = 𝐵 → ⟨𝑏, 𝑑⟩ = ⟨𝐵, 𝑑⟩)
13	12	breq1d 5042	. . . 4 ⊢ (𝑏 = 𝐵 → (⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩ ↔ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩))
14	13	anbi2d 631	. . 3 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩) ↔ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩)))
15	9, 11, 14	3anbi123d 1433	. 2 ⊢ (𝑏 = 𝐵 → ((𝐴 Colinear ⟨𝑏, 𝑐⟩ ∧ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝐵, 𝑐⟩ ∧ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩))))
16		opeq2 4763	. . . 4 ⊢ (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
17	16	breq2d 5044	. . 3 ⊢ (𝑐 = 𝐶 → (𝐴 Colinear ⟨𝐵, 𝑐⟩ ↔ 𝐴 Colinear ⟨𝐵, 𝐶⟩))
18	16	opeq2d 4770	. . . 4 ⊢ (𝑐 = 𝐶 → ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
19	18	breq1d 5042	. . 3 ⊢ (𝑐 = 𝐶 → (⟨𝐴, ⟨𝐵, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩))
20	17, 19	3anbi12d 1434	. 2 ⊢ (𝑐 = 𝐶 → ((𝐴 Colinear ⟨𝐵, 𝑐⟩ ∧ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩))))
21		opeq2 4763	. . . . 5 ⊢ (𝑑 = 𝐷 → ⟨𝐴, 𝑑⟩ = ⟨𝐴, 𝐷⟩)
22	21	breq1d 5042	. . . 4 ⊢ (𝑑 = 𝐷 → (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩))
23		opeq2 4763	. . . . 5 ⊢ (𝑑 = 𝐷 → ⟨𝐵, 𝑑⟩ = ⟨𝐵, 𝐷⟩)
24	23	breq1d 5042	. . . 4 ⊢ (𝑑 = 𝐷 → (⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩))
25	22, 24	anbi12d 633	. . 3 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩)))
26	25	3anbi3d 1439	. 2 ⊢ (𝑑 = 𝐷 → ((𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝑑⟩Cgr⟨𝑓, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩))))
27		opeq1 4761	. . . 4 ⊢ (𝑒 = 𝐸 → ⟨𝑒, ⟨𝑓, 𝑔⟩⟩ = ⟨𝐸, ⟨𝑓, 𝑔⟩⟩)
28	27	breq2d 5044	. . 3 ⊢ (𝑒 = 𝐸 → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝑓, 𝑔⟩⟩))
29		opeq1 4761	. . . . 5 ⊢ (𝑒 = 𝐸 → ⟨𝑒, ℎ⟩ = ⟨𝐸, ℎ⟩)
30	29	breq2d 5044	. . . 4 ⊢ (𝑒 = 𝐸 → (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩))
31	30	anbi1d 632	. . 3 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩)))
32	28, 31	3anbi23d 1436	. 2 ⊢ (𝑒 = 𝐸 → ((𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩))))
33		opeq1 4761	. . . . 5 ⊢ (𝑓 = 𝐹 → ⟨𝑓, 𝑔⟩ = ⟨𝐹, 𝑔⟩)
34	33	opeq2d 4770	. . . 4 ⊢ (𝑓 = 𝐹 → ⟨𝐸, ⟨𝑓, 𝑔⟩⟩ = ⟨𝐸, ⟨𝐹, 𝑔⟩⟩)
35	34	breq2d 5044	. . 3 ⊢ (𝑓 = 𝐹 → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝑓, 𝑔⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝑔⟩⟩))
36		opeq1 4761	. . . . 5 ⊢ (𝑓 = 𝐹 → ⟨𝑓, ℎ⟩ = ⟨𝐹, ℎ⟩)
37	36	breq2d 5044	. . . 4 ⊢ (𝑓 = 𝐹 → (⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩))
38	37	anbi2d 631	. . 3 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩)))
39	35, 38	3anbi23d 1436	. 2 ⊢ (𝑓 = 𝐹 → ((𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝑓, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝑔⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩))))
40		opeq2 4763	. . . . 5 ⊢ (𝑔 = 𝐺 → ⟨𝐹, 𝑔⟩ = ⟨𝐹, 𝐺⟩)
41	40	opeq2d 4770	. . . 4 ⊢ (𝑔 = 𝐺 → ⟨𝐸, ⟨𝐹, 𝑔⟩⟩ = ⟨𝐸, ⟨𝐹, 𝐺⟩⟩)
42	41	breq2d 5044	. . 3 ⊢ (𝑔 = 𝐺 → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝑔⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝐺⟩⟩))
43	42	3anbi2d 1438	. 2 ⊢ (𝑔 = 𝐺 → ((𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝑔⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝐺⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩))))
44		opeq2 4763	. . . . 5 ⊢ (ℎ = 𝐻 → ⟨𝐸, ℎ⟩ = ⟨𝐸, 𝐻⟩)
45	44	breq2d 5044	. . . 4 ⊢ (ℎ = 𝐻 → (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ↔ ⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩))
46		opeq2 4763	. . . . 5 ⊢ (ℎ = 𝐻 → ⟨𝐹, ℎ⟩ = ⟨𝐹, 𝐻⟩)
47	46	breq2d 5044	. . . 4 ⊢ (ℎ = 𝐻 → (⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩ ↔ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))
48	45, 47	anbi12d 633	. . 3 ⊢ (ℎ = 𝐻 → ((⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩) ↔ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩)))
49	48	3anbi3d 1439	. 2 ⊢ (ℎ = 𝐻 → ((𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝐺⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, ℎ⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, ℎ⟩)) ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝐺⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))
50		fveq2 6658	. 2 ⊢ (𝑛 = 𝑁 → (𝔼‘𝑛) = (𝔼‘𝑁))
51		df-fs 33893	. 2 ⊢ FiveSeg = {⟨𝑝, 𝑞⟩ ∣ ∃𝑛 ∈ ℕ ∃𝑎 ∈ (𝔼‘𝑛)∃𝑏 ∈ (𝔼‘𝑛)∃𝑐 ∈ (𝔼‘𝑛)∃𝑑 ∈ (𝔼‘𝑛)∃𝑒 ∈ (𝔼‘𝑛)∃𝑓 ∈ (𝔼‘𝑛)∃𝑔 ∈ (𝔼‘𝑛)∃ℎ ∈ (𝔼‘𝑛)(𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ (𝑎 Colinear ⟨𝑏, 𝑐⟩ ∧ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩Cgr3⟨𝑒, ⟨𝑓, 𝑔⟩⟩ ∧ (⟨𝑎, 𝑑⟩Cgr⟨𝑒, ℎ⟩ ∧ ⟨𝑏, 𝑑⟩Cgr⟨𝑓, ℎ⟩)))}
52	7, 15, 20, 26, 32, 39, 43, 49, 50, 51	br8 33239	1 ⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ (𝔼‘𝑁) ∧ 𝐵 ∈ (𝔼‘𝑁)) ∧ (𝐶 ∈ (𝔼‘𝑁) ∧ 𝐷 ∈ (𝔼‘𝑁) ∧ 𝐸 ∈ (𝔼‘𝑁)) ∧ (𝐹 ∈ (𝔼‘𝑁) ∧ 𝐺 ∈ (𝔼‘𝑁) ∧ 𝐻 ∈ (𝔼‘𝑁))) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ FiveSeg ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ (𝐴 Colinear ⟨𝐵, 𝐶⟩ ∧ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩Cgr3⟨𝐸, ⟨𝐹, 𝐺⟩⟩ ∧ (⟨𝐴, 𝐷⟩Cgr⟨𝐸, 𝐻⟩ ∧ ⟨𝐵, 𝐷⟩Cgr⟨𝐹, 𝐻⟩))))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  ⟨cop 4528   class class class wbr 5032  ‘cfv 6335  ℕcn 11674  𝔼cee 26781  Cgrccgr 26783  Cgr3ccgr3 33887   Colinear ccolin 33888   FiveSeg cfs 33889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-iota 6294  df-fv 6343  df-fs 33893

This theorem is referenced by:  fscgr  33931  linecgr  33932