Theorem dfac9 9548

Description: Equivalence of the axiom of choice with a statement related to ac9 9891; 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 9533	. 2 ⊢ (CHOICE ↔ ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
2		vex 3489	. . . . . . 7 ⊢ 𝑓 ∈ V
3	2	rnex 7603	. . . . . 6 ⊢ ran 𝑓 ∈ V
4		raleq 3405	. . . . . . 7 ⊢ (𝑠 = ran 𝑓 → (∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
5	4	exbidv 1922	. . . . . 6 ⊢ (𝑠 = ran 𝑓 → (∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
6	3, 5	spcv 3598	. . . . 5 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
7		df-nel 3124	. . . . . . . . . . . . . . 15 ⊢ (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ ran 𝑓)
8	7	biimpi 218	. . . . . . . . . . . . . 14 ⊢ (∅ ∉ ran 𝑓 → ¬ ∅ ∈ ran 𝑓)
9	8	ad2antlr 725	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ¬ ∅ ∈ ran 𝑓)
10		fvelrn 6830	. . . . . . . . . . . . . . . 16 ⊢ ((Fun 𝑓 ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
11	10	adantlr 713	. . . . . . . . . . . . . . 15 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
12		eleq1 2900	. . . . . . . . . . . . . . 15 ⊢ ((𝑓‘𝑥) = ∅ → ((𝑓‘𝑥) ∈ ran 𝑓 ↔ ∅ ∈ ran 𝑓))
13	11, 12	syl5ibcom 247	. . . . . . . . . . . . . 14 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) = ∅ → ∅ ∈ ran 𝑓))
14	13	necon3bd 3030	. . . . . . . . . . . . 13 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (¬ ∅ ∈ ran 𝑓 → (𝑓‘𝑥) ≠ ∅))
15	9, 14	mpd 15	. . . . . . . . . . . 12 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅)
16	15	adantlr 713	. . . . . . . . . . 11 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ≠ ∅)
17		neeq1 3078	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑡 ≠ ∅ ↔ (𝑓‘𝑥) ≠ ∅))
18		fveq2 6656	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → (𝑔‘𝑡) = (𝑔‘(𝑓‘𝑥)))
19		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑡 = (𝑓‘𝑥) → 𝑡 = (𝑓‘𝑥))
20	18, 19	eleq12d 2907	. . . . . . . . . . . . 13 ⊢ (𝑡 = (𝑓‘𝑥) → ((𝑔‘𝑡) ∈ 𝑡 ↔ (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
21	17, 20	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑡 = (𝑓‘𝑥) → ((𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))))
22		simplr 767	. . . . . . . . . . . 12 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
23	10	ad4ant14 750	. . . . . . . . . . . 12 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑓‘𝑥) ∈ ran 𝑓)
24	21, 22, 23	rspcdva 3617	. . . . . . . . . . 11 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → ((𝑓‘𝑥) ≠ ∅ → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
25	16, 24	mpd 15	. . . . . . . . . 10 ⊢ ((((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) ∧ 𝑥 ∈ dom 𝑓) → (𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
26	25	ralrimiva 3182	. . . . . . . . 9 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
27	2	dmex 7602	. . . . . . . . . 10 ⊢ dom 𝑓 ∈ V
28		mptelixpg 8485	. . . . . . . . . 10 ⊢ (dom 𝑓 ∈ V → ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥)))
29	27, 28	ax-mp 5	. . . . . . . . 9 ⊢ ((𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ↔ ∀𝑥 ∈ dom 𝑓(𝑔‘(𝑓‘𝑥)) ∈ (𝑓‘𝑥))
30	26, 29	sylibr 236	. . . . . . . 8 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → (𝑥 ∈ dom 𝑓 ↦ (𝑔‘(𝑓‘𝑥))) ∈ X𝑥 ∈ dom 𝑓(𝑓‘𝑥))
31	30	ne0d 4287	. . . . . . 7 ⊢ (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ∧ ∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅)
32	31	ex 415	. . . . . 6 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
33	32	exlimdv 1934	. . . . 5 ⊢ ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → (∃𝑔∀𝑡 ∈ ran 𝑓(𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
34	6, 33	syl5com 31	. . . 4 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
35	34	alrimiv 1928	. . 3 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) → ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
36		fnresi 6462	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅})
37		fnfun 6439	. . . . . . 7 ⊢ (( I ↾ (𝑠 ∖ {∅})) Fn (𝑠 ∖ {∅}) → Fun ( I ↾ (𝑠 ∖ {∅})))
38	36, 37	ax-mp 5	. . . . . 6 ⊢ Fun ( I ↾ (𝑠 ∖ {∅}))
39		neldifsn 4711	. . . . . 6 ⊢ ¬ ∅ ∈ (𝑠 ∖ {∅})
40		vex 3489	. . . . . . . . 9 ⊢ 𝑠 ∈ V
41	40	difexi 5218	. . . . . . . 8 ⊢ (𝑠 ∖ {∅}) ∈ V
42		resiexg 7605	. . . . . . . 8 ⊢ ((𝑠 ∖ {∅}) ∈ V → ( I ↾ (𝑠 ∖ {∅})) ∈ V)
43	41, 42	ax-mp 5	. . . . . . 7 ⊢ ( I ↾ (𝑠 ∖ {∅})) ∈ V
44		funeq 6361	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (Fun 𝑓 ↔ Fun ( I ↾ (𝑠 ∖ {∅}))))
45		rneq 5792	. . . . . . . . . . . . 13 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = ran ( I ↾ (𝑠 ∖ {∅})))
46		rnresi 5929	. . . . . . . . . . . . 13 ⊢ ran ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
47	45, 46	syl6eq 2872	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ran 𝑓 = (𝑠 ∖ {∅}))
48	47	eleq2d 2898	. . . . . . . . . . 11 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∈ ran 𝑓 ↔ ∅ ∈ (𝑠 ∖ {∅})))
49	48	notbid 320	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (¬ ∅ ∈ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
50	7, 49	syl5bb 285	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (∅ ∉ ran 𝑓 ↔ ¬ ∅ ∈ (𝑠 ∖ {∅})))
51	44, 50	anbi12d 632	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → ((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) ↔ (Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅}))))
52		dmeq 5758	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = dom ( I ↾ (𝑠 ∖ {∅})))
53		dmresi 5907	. . . . . . . . . . . 12 ⊢ dom ( I ↾ (𝑠 ∖ {∅})) = (𝑠 ∖ {∅})
54	52, 53	syl6eq 2872	. . . . . . . . . . 11 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → dom 𝑓 = (𝑠 ∖ {∅}))
55	54	ixpeq1d 8459	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥))
56		fveq1 6655	. . . . . . . . . . . 12 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = (( I ↾ (𝑠 ∖ {∅}))‘𝑥))
57		fvresi 6921	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) → (( I ↾ (𝑠 ∖ {∅}))‘𝑥) = 𝑥)
58	56, 57	sylan9eq 2876	. . . . . . . . . . 11 ⊢ ((𝑓 = ( I ↾ (𝑠 ∖ {∅})) ∧ 𝑥 ∈ (𝑠 ∖ {∅})) → (𝑓‘𝑥) = 𝑥)
59	58	ixpeq2dva 8462	. . . . . . . . . 10 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
60	55, 59	eqtrd 2856	. . . . . . . . 9 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) = X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
61	60	neeq1d 3075	. . . . . . . 8 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅ ↔ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
62	51, 61	imbi12d 347	. . . . . . 7 ⊢ (𝑓 = ( I ↾ (𝑠 ∖ {∅})) → (((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) ↔ ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)))
63	43, 62	spcv 3598	. . . . . 6 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ((Fun ( I ↾ (𝑠 ∖ {∅})) ∧ ¬ ∅ ∈ (𝑠 ∖ {∅})) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅))
64	38, 39, 63	mp2ani 696	. . . . 5 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅)
65		n0 4296	. . . . . 6 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ ↔ ∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥)
66		vex 3489	. . . . . . . . 9 ⊢ 𝑔 ∈ V
67	66	elixp 8454	. . . . . . . 8 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ↔ (𝑔 Fn (𝑠 ∖ {∅}) ∧ ∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥))
68		eldifsn 4705	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑠 ∖ {∅}) ↔ (𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅))
69	68	imbi1i 352	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ ((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥))
70		impexp 453	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝑠 ∧ 𝑥 ≠ ∅) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
71	69, 70	bitri 277	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (𝑠 ∖ {∅}) → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑥 ∈ 𝑠 → (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥)))
72	71	ralbii2 3163	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥))
73		neeq1 3078	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → (𝑥 ≠ ∅ ↔ 𝑡 ≠ ∅))
74		fveq2 6656	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → (𝑔‘𝑥) = (𝑔‘𝑡))
75		id 22	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑡 → 𝑥 = 𝑡)
76	74, 75	eleq12d 2907	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑡 → ((𝑔‘𝑥) ∈ 𝑥 ↔ (𝑔‘𝑡) ∈ 𝑡))
77	73, 76	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑡 → ((𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡)))
78	77	cbvralvw 3441	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ 𝑠 (𝑥 ≠ ∅ → (𝑔‘𝑥) ∈ 𝑥) ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
79	72, 78	bitri 277	. . . . . . . . 9 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 ↔ ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
80	79	biimpi 218	. . . . . . . 8 ⊢ (∀𝑥 ∈ (𝑠 ∖ {∅})(𝑔‘𝑥) ∈ 𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
81	67, 80	simplbiim 507	. . . . . . 7 ⊢ (𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
82	81	eximi 1835	. . . . . 6 ⊢ (∃𝑔 𝑔 ∈ X𝑥 ∈ (𝑠 ∖ {∅})𝑥 → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
83	65, 82	sylbi 219	. . . . 5 ⊢ (X𝑥 ∈ (𝑠 ∖ {∅})𝑥 ≠ ∅ → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
84	64, 83	syl 17	. . . 4 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
85	84	alrimiv 1928	. . 3 ⊢ (∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅) → ∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡))
86	35, 85	impbii 211	. 2 ⊢ (∀𝑠∃𝑔∀𝑡 ∈ 𝑠 (𝑡 ≠ ∅ → (𝑔‘𝑡) ∈ 𝑡) ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))
87	1, 86	bitri 277	1 ⊢ (CHOICE ↔ ∀𝑓((Fun 𝑓 ∧ ∅ ∉ ran 𝑓) → X𝑥 ∈ dom 𝑓(𝑓‘𝑥) ≠ ∅))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537  ∃wex 1780   ∈ wcel 2114   ≠ wne 3016   ∉ wnel 3123  ∀wral 3138  Vcvv 3486   ∖ cdif 3921  ∅c0 4279  {csn 4553   ↦ cmpt 5132   I cid 5445  dom cdm 5541  ran crn 5542   ↾ cres 5543  Fun wfun 6335   Fn wfn 6336  ‘cfv 6341  Xcixp 8447  CHOICEwac 9527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ixp 8448  df-ac 9528

This theorem is referenced by:  dfac14  22209  dfac21  39758