Theorem undmrnresiss 40304

Description: Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg 40305. (Contributed by RP, 26-Sep-2020.)

Assertion

Ref	Expression
undmrnresiss	⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem undmrnresiss

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		resundi 5832	. . 3 ⊢ ( I ↾ (dom 𝐴 ∪ ran 𝐴)) = (( I ↾ dom 𝐴) ∪ ( I ↾ ran 𝐴))
2	1	sseq1i 3943	. 2 ⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ (( I ↾ dom 𝐴) ∪ ( I ↾ ran 𝐴)) ⊆ 𝐵)
3		unss 4111	. 2 ⊢ ((( I ↾ dom 𝐴) ⊆ 𝐵 ∧ ( I ↾ ran 𝐴) ⊆ 𝐵) ↔ (( I ↾ dom 𝐴) ∪ ( I ↾ ran 𝐴)) ⊆ 𝐵)
4		relres 5847	. . . . . 6 ⊢ Rel ( I ↾ dom 𝐴)
5		ssrel 5621	. . . . . 6 ⊢ (Rel ( I ↾ dom 𝐴) → (( I ↾ dom 𝐴) ⊆ 𝐵 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ( I ↾ dom 𝐴) → ⟨𝑥, 𝑧⟩ ∈ 𝐵)))
6	4, 5	ax-mp 5	. . . . 5 ⊢ (( I ↾ dom 𝐴) ⊆ 𝐵 ↔ ∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ( I ↾ dom 𝐴) → ⟨𝑥, 𝑧⟩ ∈ 𝐵))
7		vex 3444	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
8	7	eldm 5733	. . . . . . . . 9 ⊢ (𝑥 ∈ dom 𝐴 ↔ ∃𝑦 𝑥𝐴𝑦)
9		df-br 5031	. . . . . . . . . 10 ⊢ (𝑥 I 𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ I )
10		vex 3444	. . . . . . . . . . 11 ⊢ 𝑧 ∈ V
11	10	ideq 5687	. . . . . . . . . 10 ⊢ (𝑥 I 𝑧 ↔ 𝑥 = 𝑧)
12	9, 11	bitr3i 280	. . . . . . . . 9 ⊢ (⟨𝑥, 𝑧⟩ ∈ I ↔ 𝑥 = 𝑧)
13	8, 12	anbi12ci 630	. . . . . . . 8 ⊢ ((𝑥 ∈ dom 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ I ) ↔ (𝑥 = 𝑧 ∧ ∃𝑦 𝑥𝐴𝑦))
14	10	opelresi 5826	. . . . . . . 8 ⊢ (⟨𝑥, 𝑧⟩ ∈ ( I ↾ dom 𝐴) ↔ (𝑥 ∈ dom 𝐴 ∧ ⟨𝑥, 𝑧⟩ ∈ I ))
15		19.42v 1954	. . . . . . . 8 ⊢ (∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) ↔ (𝑥 = 𝑧 ∧ ∃𝑦 𝑥𝐴𝑦))
16	13, 14, 15	3bitr4i 306	. . . . . . 7 ⊢ (⟨𝑥, 𝑧⟩ ∈ ( I ↾ dom 𝐴) ↔ ∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦))
17		df-br 5031	. . . . . . . 8 ⊢ (𝑥𝐵𝑧 ↔ ⟨𝑥, 𝑧⟩ ∈ 𝐵)
18	17	bicomi 227	. . . . . . 7 ⊢ (⟨𝑥, 𝑧⟩ ∈ 𝐵 ↔ 𝑥𝐵𝑧)
19	16, 18	imbi12i 354	. . . . . 6 ⊢ ((⟨𝑥, 𝑧⟩ ∈ ( I ↾ dom 𝐴) → ⟨𝑥, 𝑧⟩ ∈ 𝐵) ↔ (∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧))
20	19	2albii 1822	. . . . 5 ⊢ (∀𝑥∀𝑧(⟨𝑥, 𝑧⟩ ∈ ( I ↾ dom 𝐴) → ⟨𝑥, 𝑧⟩ ∈ 𝐵) ↔ ∀𝑥∀𝑧(∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧))
21		19.23v 1943	. . . . . . . 8 ⊢ (∀𝑦((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ (∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧))
22	21	bicomi 227	. . . . . . 7 ⊢ ((∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑦((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧))
23	22	2albii 1822	. . . . . 6 ⊢ (∀𝑥∀𝑧(∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑥∀𝑧∀𝑦((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧))
24		alcom 2160	. . . . . . . 8 ⊢ (∀𝑧∀𝑦((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑦∀𝑧((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧))
25		ancomst 468	. . . . . . . . . . . 12 ⊢ (((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ((𝑥𝐴𝑦 ∧ 𝑥 = 𝑧) → 𝑥𝐵𝑧))
26		impexp 454	. . . . . . . . . . . 12 ⊢ (((𝑥𝐴𝑦 ∧ 𝑥 = 𝑧) → 𝑥𝐵𝑧) ↔ (𝑥𝐴𝑦 → (𝑥 = 𝑧 → 𝑥𝐵𝑧)))
27	25, 26	bitri 278	. . . . . . . . . . 11 ⊢ (((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ (𝑥𝐴𝑦 → (𝑥 = 𝑧 → 𝑥𝐵𝑧)))
28	27	albii 1821	. . . . . . . . . 10 ⊢ (∀𝑧((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑧(𝑥𝐴𝑦 → (𝑥 = 𝑧 → 𝑥𝐵𝑧)))
29		19.21v 1940	. . . . . . . . . 10 ⊢ (∀𝑧(𝑥𝐴𝑦 → (𝑥 = 𝑧 → 𝑥𝐵𝑧)) ↔ (𝑥𝐴𝑦 → ∀𝑧(𝑥 = 𝑧 → 𝑥𝐵𝑧)))
30		equcom 2025	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥)
31	30	imbi1i 353	. . . . . . . . . . . . 13 ⊢ ((𝑥 = 𝑧 → 𝑥𝐵𝑧) ↔ (𝑧 = 𝑥 → 𝑥𝐵𝑧))
32	31	albii 1821	. . . . . . . . . . . 12 ⊢ (∀𝑧(𝑥 = 𝑧 → 𝑥𝐵𝑧) ↔ ∀𝑧(𝑧 = 𝑥 → 𝑥𝐵𝑧))
33		breq2 5034	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑥 → (𝑥𝐵𝑧 ↔ 𝑥𝐵𝑥))
34	33	equsalvw 2010	. . . . . . . . . . . 12 ⊢ (∀𝑧(𝑧 = 𝑥 → 𝑥𝐵𝑧) ↔ 𝑥𝐵𝑥)
35	32, 34	bitri 278	. . . . . . . . . . 11 ⊢ (∀𝑧(𝑥 = 𝑧 → 𝑥𝐵𝑧) ↔ 𝑥𝐵𝑥)
36	35	imbi2i 339	. . . . . . . . . 10 ⊢ ((𝑥𝐴𝑦 → ∀𝑧(𝑥 = 𝑧 → 𝑥𝐵𝑧)) ↔ (𝑥𝐴𝑦 → 𝑥𝐵𝑥))
37	28, 29, 36	3bitri 300	. . . . . . . . 9 ⊢ (∀𝑧((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ (𝑥𝐴𝑦 → 𝑥𝐵𝑥))
38	37	albii 1821	. . . . . . . 8 ⊢ (∀𝑦∀𝑧((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑥))
39	24, 38	bitri 278	. . . . . . 7 ⊢ (∀𝑧∀𝑦((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑥))
40	39	albii 1821	. . . . . 6 ⊢ (∀𝑥∀𝑧∀𝑦((𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑥))
41	23, 40	bitri 278	. . . . 5 ⊢ (∀𝑥∀𝑧(∃𝑦(𝑥 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑥𝐵𝑧) ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑥))
42	6, 20, 41	3bitri 300	. . . 4 ⊢ (( I ↾ dom 𝐴) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑥))
43		relres 5847	. . . . . 6 ⊢ Rel ( I ↾ ran 𝐴)
44		ssrel 5621	. . . . . 6 ⊢ (Rel ( I ↾ ran 𝐴) → (( I ↾ ran 𝐴) ⊆ 𝐵 ↔ ∀𝑦∀𝑧(⟨𝑦, 𝑧⟩ ∈ ( I ↾ ran 𝐴) → ⟨𝑦, 𝑧⟩ ∈ 𝐵)))
45	43, 44	ax-mp 5	. . . . 5 ⊢ (( I ↾ ran 𝐴) ⊆ 𝐵 ↔ ∀𝑦∀𝑧(⟨𝑦, 𝑧⟩ ∈ ( I ↾ ran 𝐴) → ⟨𝑦, 𝑧⟩ ∈ 𝐵))
46		vex 3444	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
47	46	elrn 5786	. . . . . . . . 9 ⊢ (𝑦 ∈ ran 𝐴 ↔ ∃𝑥 𝑥𝐴𝑦)
48		df-br 5031	. . . . . . . . . 10 ⊢ (𝑦 I 𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ I )
49	10	ideq 5687	. . . . . . . . . 10 ⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧)
50	48, 49	bitr3i 280	. . . . . . . . 9 ⊢ (⟨𝑦, 𝑧⟩ ∈ I ↔ 𝑦 = 𝑧)
51	47, 50	anbi12ci 630	. . . . . . . 8 ⊢ ((𝑦 ∈ ran 𝐴 ∧ ⟨𝑦, 𝑧⟩ ∈ I ) ↔ (𝑦 = 𝑧 ∧ ∃𝑥 𝑥𝐴𝑦))
52	10	opelresi 5826	. . . . . . . 8 ⊢ (⟨𝑦, 𝑧⟩ ∈ ( I ↾ ran 𝐴) ↔ (𝑦 ∈ ran 𝐴 ∧ ⟨𝑦, 𝑧⟩ ∈ I ))
53		19.42v 1954	. . . . . . . 8 ⊢ (∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) ↔ (𝑦 = 𝑧 ∧ ∃𝑥 𝑥𝐴𝑦))
54	51, 52, 53	3bitr4i 306	. . . . . . 7 ⊢ (⟨𝑦, 𝑧⟩ ∈ ( I ↾ ran 𝐴) ↔ ∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦))
55		df-br 5031	. . . . . . . 8 ⊢ (𝑦𝐵𝑧 ↔ ⟨𝑦, 𝑧⟩ ∈ 𝐵)
56	55	bicomi 227	. . . . . . 7 ⊢ (⟨𝑦, 𝑧⟩ ∈ 𝐵 ↔ 𝑦𝐵𝑧)
57	54, 56	imbi12i 354	. . . . . 6 ⊢ ((⟨𝑦, 𝑧⟩ ∈ ( I ↾ ran 𝐴) → ⟨𝑦, 𝑧⟩ ∈ 𝐵) ↔ (∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧))
58	57	2albii 1822	. . . . 5 ⊢ (∀𝑦∀𝑧(⟨𝑦, 𝑧⟩ ∈ ( I ↾ ran 𝐴) → ⟨𝑦, 𝑧⟩ ∈ 𝐵) ↔ ∀𝑦∀𝑧(∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧))
59		19.23v 1943	. . . . . . . 8 ⊢ (∀𝑥((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ (∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧))
60	59	bicomi 227	. . . . . . 7 ⊢ ((∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ ∀𝑥((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧))
61	60	2albii 1822	. . . . . 6 ⊢ (∀𝑦∀𝑧(∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ ∀𝑦∀𝑧∀𝑥((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧))
62		alrot3 2161	. . . . . 6 ⊢ (∀𝑥∀𝑦∀𝑧((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ ∀𝑦∀𝑧∀𝑥((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧))
63		ancomst 468	. . . . . . . . . 10 ⊢ (((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ ((𝑥𝐴𝑦 ∧ 𝑦 = 𝑧) → 𝑦𝐵𝑧))
64		impexp 454	. . . . . . . . . 10 ⊢ (((𝑥𝐴𝑦 ∧ 𝑦 = 𝑧) → 𝑦𝐵𝑧) ↔ (𝑥𝐴𝑦 → (𝑦 = 𝑧 → 𝑦𝐵𝑧)))
65	63, 64	bitri 278	. . . . . . . . 9 ⊢ (((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ (𝑥𝐴𝑦 → (𝑦 = 𝑧 → 𝑦𝐵𝑧)))
66	65	albii 1821	. . . . . . . 8 ⊢ (∀𝑧((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ ∀𝑧(𝑥𝐴𝑦 → (𝑦 = 𝑧 → 𝑦𝐵𝑧)))
67		19.21v 1940	. . . . . . . 8 ⊢ (∀𝑧(𝑥𝐴𝑦 → (𝑦 = 𝑧 → 𝑦𝐵𝑧)) ↔ (𝑥𝐴𝑦 → ∀𝑧(𝑦 = 𝑧 → 𝑦𝐵𝑧)))
68		equcom 2025	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 ↔ 𝑧 = 𝑦)
69	68	imbi1i 353	. . . . . . . . . . 11 ⊢ ((𝑦 = 𝑧 → 𝑦𝐵𝑧) ↔ (𝑧 = 𝑦 → 𝑦𝐵𝑧))
70	69	albii 1821	. . . . . . . . . 10 ⊢ (∀𝑧(𝑦 = 𝑧 → 𝑦𝐵𝑧) ↔ ∀𝑧(𝑧 = 𝑦 → 𝑦𝐵𝑧))
71		breq2 5034	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (𝑦𝐵𝑧 ↔ 𝑦𝐵𝑦))
72	71	equsalvw 2010	. . . . . . . . . 10 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝑦𝐵𝑧) ↔ 𝑦𝐵𝑦)
73	70, 72	bitri 278	. . . . . . . . 9 ⊢ (∀𝑧(𝑦 = 𝑧 → 𝑦𝐵𝑧) ↔ 𝑦𝐵𝑦)
74	73	imbi2i 339	. . . . . . . 8 ⊢ ((𝑥𝐴𝑦 → ∀𝑧(𝑦 = 𝑧 → 𝑦𝐵𝑧)) ↔ (𝑥𝐴𝑦 → 𝑦𝐵𝑦))
75	66, 67, 74	3bitri 300	. . . . . . 7 ⊢ (∀𝑧((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ (𝑥𝐴𝑦 → 𝑦𝐵𝑦))
76	75	2albii 1822	. . . . . 6 ⊢ (∀𝑥∀𝑦∀𝑧((𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑦𝐵𝑦))
77	61, 62, 76	3bitr2i 302	. . . . 5 ⊢ (∀𝑦∀𝑧(∃𝑥(𝑦 = 𝑧 ∧ 𝑥𝐴𝑦) → 𝑦𝐵𝑧) ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑦𝐵𝑦))
78	45, 58, 77	3bitri 300	. . . 4 ⊢ (( I ↾ ran 𝐴) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑦𝐵𝑦))
79	42, 78	anbi12i 629	. . 3 ⊢ ((( I ↾ dom 𝐴) ⊆ 𝐵 ∧ ( I ↾ ran 𝐴) ⊆ 𝐵) ↔ (∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑥) ∧ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑦𝐵𝑦)))
80		19.26-2 1872	. . 3 ⊢ (∀𝑥∀𝑦((𝑥𝐴𝑦 → 𝑥𝐵𝑥) ∧ (𝑥𝐴𝑦 → 𝑦𝐵𝑦)) ↔ (∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑥𝐵𝑥) ∧ ∀𝑥∀𝑦(𝑥𝐴𝑦 → 𝑦𝐵𝑦)))
81		pm4.76 522	. . . 4 ⊢ (((𝑥𝐴𝑦 → 𝑥𝐵𝑥) ∧ (𝑥𝐴𝑦 → 𝑦𝐵𝑦)) ↔ (𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))
82	81	2albii 1822	. . 3 ⊢ (∀𝑥∀𝑦((𝑥𝐴𝑦 → 𝑥𝐵𝑥) ∧ (𝑥𝐴𝑦 → 𝑦𝐵𝑦)) ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))
83	79, 80, 82	3bitr2i 302	. 2 ⊢ ((( I ↾ dom 𝐴) ⊆ 𝐵 ∧ ( I ↾ ran 𝐴) ⊆ 𝐵) ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))
84	2, 3, 83	3bitr2i 302	1 ⊢ (( I ↾ (dom 𝐴 ∪ ran 𝐴)) ⊆ 𝐵 ↔ ∀𝑥∀𝑦(𝑥𝐴𝑦 → (𝑥𝐵𝑥 ∧ 𝑦𝐵𝑦)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781   ∈ wcel 2111   ∪ cun 3879   ⊆ wss 3881  ⟨cop 4531   class class class wbr 5030   I cid 5424  dom cdm 5519  ran crn 5520   ↾ cres 5521  Rel wrel 5524

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-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531

This theorem is referenced by:  reflexg  40305