Theorem dfac9 10254

Description: Equivalence of the axiom of choice with a statement related to ac9 10600; definition AC3 of [Schechter] p. 139. (Contributed by Stefan O'Rear, 22-Feb-2015.)

Assertion

Ref	Expression
dfac9	⊢ (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))

Distinct variable group:   𝑥,𝑓

Proof of Theorem dfac9

Dummy variables 𝑔 𝑠 𝑡 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfac3 10239	. 2 ⊢ (CHOICE ↔ ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
2		vex 3458	. . . . . . 7 ⊢ 𝑓 ∈ V
3	2	rnex 7956	. . . . . 6 ⊢ ran 𝑓 ∈ V
4		raleq 3320	. . . . . . 7 ⊢ (𝑠 = ran 𝑓 → (∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
5	4	exbidv 1956	. . . . . 6 ⊢ (𝑠 = ran 𝑓 → (∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
6	3, 5	spcv 3563	. . . . 5 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
7		df-nel 3066	. . . . . . . . . . . . . . 15 ⊢ (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓)
8	7	biimpi 219	. . . . . . . . . . . . . 14 ⊢ (∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓)
9	8	ad2antlr 740	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓)
10		fvelrn 7108	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
11	10	adantlr 728	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
12		eleq1 2852	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑥) = ∅ → ((𝑓‘𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓))
13	11, 12	syl5ibcom 248	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) = ∅ → ∅ ∈ ran 𝑓))
14	13	necon3bd 2973	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (¬ ∅ ∈ ran 𝑓 → (𝑓‘𝑥) ≠ ∅))
15	9, 14	mpd 16	. . . . . . . . . . . 12 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅)
16	15	adantlr 728	. . . . . . . . . . 11 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅)
17		neeq1 3021	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑡 ≠ ∅ ↔ (𝑓‘𝑥) ≠ ∅))
18		fveq2 6916	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑔‘𝑡) = (𝑔‘(𝑓‘𝑥)))
19		id 23	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → 𝑡 = (𝑓‘𝑥))
20	18, 19	eleq12d 2858	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑓‘𝑥) → ((𝑔‘𝑡) ∈ 𝑡 ↔ (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
21	17, 20	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑓‘𝑥) → ((𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))))
22		simplr 781	. . . . . . . . . . . 12 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
23	10	ad4ant14 765	. . . . . . . . . . . 12 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
24	21, 22, 23	rspcdva 3581	. . . . . . . . . . 11 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
25	16, 24	mpd 16	. . . . . . . . . 10 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
26	25	ralrimiva 3158	. . . . . . . . 9 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
27	2	dmex 7955	. . . . . . . . . 10 ⊢ dom 𝑓 ∈ V
28		mptelixpg 9001	. . . . . . . . . 10 ⊢ (dom 𝑓 ∈ V → ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
29	27, 28	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
30	26, 29	sylibr 237	. . . . . . . 8 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → (𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥))
31	30	ne0d 4291	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)
32	31	ex 418	. . . . . 6 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
33	32	exlimdv 1968	. . . . 5 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
34	6, 33	syl5com 32	. . . 4 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
35	34	alrimiv 1962	. . 3 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
36		fnresi 6698	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅})
37		fnfun 6669	. . . . . . 7 ⊢ (( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅}) → Fun ( I ↾ (𝑠 ∖ {∅})))
38	36, 37	ax-mp 5	. . . . . 6 ⊢ Fun ( I ↾ (𝑠 ∖ {∅}))
39		neldifsn 4757	. . . . . 6 ⊢ ¬ ∅ ∈ (𝑠 ∖ {∅})
40		vex 3458	. . . . . . . . 9 ⊢ 𝑠 ∈ V
41	40	difexi 5299	. . . . . . . 8 ⊢ (𝑠 ∖ {∅}) ∈ V
42		resiexg 7958	. . . . . . . 8 ⊢ ((𝑠 ∖ {∅}) ∈ V → ( I ↾ (𝑠 ∖ {∅})) ∈ V)
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) ∈ V
44		funeq 6587	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (Fun 𝑓 ↔ Fun ( I ↾ (𝑠 ∖ {∅}))))
45		rneq 5930	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = ran ( I ↾ (𝑠 ∖ {∅})))
46		rnresi 6091	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
47	45, 46	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = (𝑠 ∖ {∅}))
48	47	eleq2d 2850	. . . . . . . . . . 11 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∈ ran 𝑓 ↔ ∅ ∈ (𝑠 ∖ {∅})))
49	48	notbid 321	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (¬ ∅ ∈ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
50	7, 49	bitrid 286	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
51	44, 50	anbi12d 644	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ↔ (Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅}))))
52		dmeq 5897	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = dom ( I ↾ (𝑠 ∖ {∅})))
53		dmresi 6062	. . . . . . . . . . . 12 ⊢ dom ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
54	52, 53	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = (𝑠 ∖ {∅}))
55	54	ixpeq1d 8975	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥))
56		fveq1 6915	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥))
57		fvresi 7209	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾ (𝑠 ∖ {∅}))‘𝑥) = 𝑥)
58	56, 57	sylan9eq 2818	. . . . . . . . . . 11 ⊢ ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = 𝑥)
59	58	ixpeq2dva 8978	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
60	55, 59	eqtrd 2798	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
61	60	neeq1d 3018	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅ ↔ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
62	51, 61	imbi12d 347	. . . . . . 7 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) ↔ ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)))
63	43, 62	spcv 3563	. . . . . 6 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
64	38, 39, 63	mp2ani 711	. . . . 5 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)
65		n0 4303	. . . . . 6 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ ↔ ∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
66		vex 3458	. . . . . . . . 9 ⊢ 𝑔 ∈ V
67	66	elixp 8970	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥))
68		eldifsn 4750	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅))
69	68	imbi1i 352	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ ((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥))
70		impexp 456	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
71	69, 70	bitri 278	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
72	71	ralbii2 3108	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))
73		neeq1 3021	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅))
74		fveq2 6916	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
75		id 23	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → 𝑥 = 𝑡)
76	74, 75	eleq12d 2858	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑡) ∈ 𝑡))
77	73, 76	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
78	77	cbvralvw 3244	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
79	72, 78	bitri 278	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
80	79	biimpi 219	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
81	67, 80	simplbiim 514	. . . . . . 7 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
82	81	eximi 1868	. . . . . 6 ⊢ (∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
83	65, 82	sylbi 220	. . . . 5 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
84	64, 83	syl 18	. . . 4 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
85	84	alrimiv 1962	. . 3 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
86	35, 85	impbii 212	. 2 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
87	1, 86	bitri 278	1 ⊢ (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ≠ wne 2959   ∉ wnel 3065  ∀wral 3080  Vcvv 3454   ∖ cdif 4048  ∅c0 4281  {csn 4588   ↦ cmpt 5192   I cid 5552  dom cdm 5658  ran crn 5659   ↾ cres 5660  Fun wfun 6560   Fn wfn 6561  ‘cfv 6566  Xcixp 8963  CHOICEwac 10233

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ixp 8964  df-ac 10234

This theorem is used by:  dfac14  23992  dfac21  44334