Theorem uchoice 6253

Description: Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7357 (with the key difference being the change of E. to E!) but unique choice in fact follows from the axiom of collection and our other axioms. This is somewhat similar to Corollary 3.9.2 of [HoTT], p. (varies) but is better described by the paragraph at the end of Section 3.9 which starts "A similar issue arises in set-theoretic mathematics". (Contributed by Jim Kingdon, 13-Sep-2025.)

Assertion

Ref	Expression
uchoice	|- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )

Distinct variable groups:   A, f, x, y   ph, f

Allowed substitution hints:   ph( x, y)   V( x, y, f)

Proof of Theorem uchoice

Dummy variables u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2209	. . . . . . . . 9 |- { <. x , y >. | ( x e. A /\ ph ) } = { <. x , y >. | ( x e. A /\ ph ) }
2	1	fnopabg 5423	. . . . . . . 8 |- ( A. x e. A E! y ph <-> { <. x , y >. | ( x e. A /\ ph ) } Fn A )
3	2	biimpi 120	. . . . . . 7 |- ( A. x e. A E! y ph -> { <. x , y >. | ( x e. A /\ ph ) } Fn A )
4	3	adantl 277	. . . . . 6 |- ( ( A e. V /\ A. x e. A E! y ph ) -> { <. x , y >. | ( x e. A /\ ph ) } Fn A )
5		simpl 109	. . . . . 6 |- ( ( A e. V /\ A. x e. A E! y ph ) -> A e. V )
6		fnex 5834	. . . . . 6 |- ( ( { <. x , y >. | ( x e. A /\ ph ) } Fn A /\ A e. V ) -> { <. x , y >. | ( x e. A /\ ph ) } e. _V )
7	4, 5, 6	syl2anc 411	. . . . 5 |- ( ( A e. V /\ A. x e. A E! y ph ) -> { <. x , y >. | ( x e. A /\ ph ) } e. _V )
8		fnopfvb 5647	. . . . . . . . . 10 |- ( ( { <. x , y >. | ( x e. A /\ ph ) } Fn A /\ u e. A ) -> ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> <. u , v >. e. { <. x , y >. | ( x e. A /\ ph ) } ) )
9		nfv 1554	. . . . . . . . . . . 12 |- F/ x u e. A
10		nfsbc1v 3027	. . . . . . . . . . . 12 |- F/ x [. u / x ]. ph
11	9, 10	nfan 1591	. . . . . . . . . . 11 |- F/ x ( u e. A /\ [. u / x ]. ph )
12		nfv 1554	. . . . . . . . . . . 12 |- F/ y u e. A
13		nfsbc1v 3027	. . . . . . . . . . . 12 |- F/ y [. v / y ]. [. u / x ]. ph
14	12, 13	nfan 1591	. . . . . . . . . . 11 |- F/ y ( u e. A /\ [. v / y ]. [. u / x ]. ph )
15		vex 2782	. . . . . . . . . . 11 |- u e. _V
16		vex 2782	. . . . . . . . . . 11 |- v e. _V
17		eleq1w 2270	. . . . . . . . . . . 12 |- ( x = u -> ( x e. A <-> u e. A ) )
18		sbceq1a 3018	. . . . . . . . . . . 12 |- ( x = u -> ( ph <-> [. u / x ]. ph ) )
19	17, 18	anbi12d 473	. . . . . . . . . . 11 |- ( x = u -> ( ( x e. A /\ ph ) <-> ( u e. A /\ [. u / x ]. ph ) ) )
20		sbceq1a 3018	. . . . . . . . . . . 12 |- ( y = v -> ( [. u / x ]. ph <-> [. v / y ]. [. u / x ]. ph ) )
21	20	anbi2d 464	. . . . . . . . . . 11 |- ( y = v -> ( ( u e. A /\ [. u / x ]. ph ) <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) )
22	11, 14, 15, 16, 19, 21	opelopabf 4342	. . . . . . . . . 10 |- ( <. u , v >. e. { <. x , y >. | ( x e. A /\ ph ) } <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) )
23	8, 22	bitrdi 196	. . . . . . . . 9 |- ( ( { <. x , y >. | ( x e. A /\ ph ) } Fn A /\ u e. A ) -> ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) )
24	23	ralrimiva 2583	. . . . . . . 8 |- ( { <. x , y >. | ( x e. A /\ ph ) } Fn A -> A. u e. A ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) )
25	24	alrimiv 1900	. . . . . . 7 |- ( { <. x , y >. | ( x e. A /\ ph ) } Fn A -> A. v A. u e. A ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) )
26	25	ancli 323	. . . . . 6 |- ( { <. x , y >. | ( x e. A /\ ph ) } Fn A -> ( { <. x , y >. | ( x e. A /\ ph ) } Fn A /\ A. v A. u e. A ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
27	4, 26	syl 14	. . . . 5 |- ( ( A e. V /\ A. x e. A E! y ph ) -> ( { <. x , y >. | ( x e. A /\ ph ) } Fn A /\ A. v A. u e. A ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
28		fneq1 5385	. . . . . 6 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( f Fn A <-> { <. x , y >. | ( x e. A /\ ph ) } Fn A ) )
29		fveq1 5602	. . . . . . . . . 10 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( f ` u ) = ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) )
30	29	eqeq1d 2218	. . . . . . . . 9 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( ( f ` u ) = v <-> ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v ) )
31	30	bibi1d 233	. . . . . . . 8 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) <-> ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
32	31	ralbidv 2510	. . . . . . 7 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( A. u e. A ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) <-> A. u e. A ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
33	32	albidv 1850	. . . . . 6 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( A. v A. u e. A ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) <-> A. v A. u e. A ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
34	28, 33	anbi12d 473	. . . . 5 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( ( f Fn A /\ A. v A. u e. A ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) <-> ( { <. x , y >. | ( x e. A /\ ph ) } Fn A /\ A. v A. u e. A ( ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) ) )
35	7, 27, 34	elabd 2928	. . . 4 |- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. v A. u e. A ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
36		ralcom4 2802	. . . . . 6 |- ( A. u e. A A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) <-> A. v A. u e. A ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) )
37	36	anbi2i 457	. . . . 5 |- ( ( f Fn A /\ A. u e. A A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) <-> ( f Fn A /\ A. v A. u e. A ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
38	37	exbii 1631	. . . 4 |- ( E. f ( f Fn A /\ A. u e. A A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) <-> E. f ( f Fn A /\ A. v A. u e. A ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
39	35, 38	sylibr 134	. . 3 |- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. u e. A A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) )
40		nfv 1554	. . . . . . . 8 |- F/ x ( f ` u ) = v
41		nfcv 2352	. . . . . . . . . 10 |- F/_ x v
42	41, 10	nfsbc 3029	. . . . . . . . 9 |- F/ x [. v / y ]. [. u / x ]. ph
43	9, 42	nfan 1591	. . . . . . . 8 |- F/ x ( u e. A /\ [. v / y ]. [. u / x ]. ph )
44	40, 43	nfbi 1615	. . . . . . 7 |- F/ x ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) )
45	44	nfal 1602	. . . . . 6 |- F/ x A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) )
46		nfv 1554	. . . . . 6 |- F/ u A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) )
47		fveqeq2 5612	. . . . . . . 8 |- ( u = x -> ( ( f ` u ) = v <-> ( f ` x ) = v ) )
48		eleq1w 2270	. . . . . . . . 9 |- ( u = x -> ( u e. A <-> x e. A ) )
49		sbceq2a 3019	. . . . . . . . . 10 |- ( u = x -> ( [. u / x ]. ph <-> ph ) )
50	49	sbcbidv 3067	. . . . . . . . 9 |- ( u = x -> ( [. v / y ]. [. u / x ]. ph <-> [. v / y ]. ph ) )
51	48, 50	anbi12d 473	. . . . . . . 8 |- ( u = x -> ( ( u e. A /\ [. v / y ]. [. u / x ]. ph ) <-> ( x e. A /\ [. v / y ]. ph ) ) )
52	47, 51	bibi12d 235	. . . . . . 7 |- ( u = x -> ( ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) <-> ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) ) )
53	52	albidv 1850	. . . . . 6 |- ( u = x -> ( A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) <-> A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) ) )
54	45, 46, 53	cbvral 2741	. . . . 5 |- ( A. u e. A A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) <-> A. x e. A A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) )
55	54	anbi2i 457	. . . 4 |- ( ( f Fn A /\ A. u e. A A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) <-> ( f Fn A /\ A. x e. A A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) ) )
56	55	exbii 1631	. . 3 |- ( E. f ( f Fn A /\ A. u e. A A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) ) ) <-> E. f ( f Fn A /\ A. x e. A A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) ) )
57	39, 56	sylib 122	. 2 |- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. x e. A A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) ) )
58		eqidd 2210	. . . . . . 7 |- ( A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) -> ( f ` x ) = ( f ` x ) )
59		vex 2782	. . . . . . . . 9 |- f e. _V
60		vex 2782	. . . . . . . . 9 |- x e. _V
61	59, 60	fvex 5623	. . . . . . . 8 |- ( f ` x ) e. _V
62		eqeq2 2219	. . . . . . . . 9 |- ( v = ( f ` x ) -> ( ( f ` x ) = v <-> ( f ` x ) = ( f ` x ) ) )
63		dfsbcq 3010	. . . . . . . . . 10 |- ( v = ( f ` x ) -> ( [. v / y ]. ph <-> [. ( f ` x ) / y ]. ph ) )
64	63	anbi2d 464	. . . . . . . . 9 |- ( v = ( f ` x ) -> ( ( x e. A /\ [. v / y ]. ph ) <-> ( x e. A /\ [. ( f ` x ) / y ]. ph ) ) )
65	62, 64	bibi12d 235	. . . . . . . 8 |- ( v = ( f ` x ) -> ( ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) <-> ( ( f ` x ) = ( f ` x ) <-> ( x e. A /\ [. ( f ` x ) / y ]. ph ) ) ) )
66	61, 65	spcv 2877	. . . . . . 7 |- ( A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) -> ( ( f ` x ) = ( f ` x ) <-> ( x e. A /\ [. ( f ` x ) / y ]. ph ) ) )
67	58, 66	mpbid 147	. . . . . 6 |- ( A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) -> ( x e. A /\ [. ( f ` x ) / y ]. ph ) )
68	67	simprd 114	. . . . 5 |- ( A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) -> [. ( f ` x ) / y ]. ph )
69	68	ralimi 2573	. . . 4 |- ( A. x e. A A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) -> A. x e. A [. ( f ` x ) / y ]. ph )
70	69	anim2i 342	. . 3 |- ( ( f Fn A /\ A. x e. A A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) ) -> ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
71	70	eximi 1626	. 2 |- ( E. f ( f Fn A /\ A. x e. A A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) ) -> E. f ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )
72	57, 71	syl 14	1 |- ( ( A e. V /\ A. x e. A E! y ph ) -> E. f ( f Fn A /\ A. x e. A [. ( f ` x ) / y ]. ph ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   A.wal 1373   = wceq 1375   E.wex 1518   E!weu 2057   e. wcel 2180   A.wral 2488   _Vcvv 2779   [.wsbc 3008   <.cop 3649   {copab 4123   Fn wfn 5289   ` cfv 5294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-13 2182  ax-14 2183  ax-ext 2191  ax-coll 4178  ax-sep 4181  ax-pow 4237  ax-pr 4272  ax-un 4501

This theorem depends on definitions:  df-bi 117  df-3an 985  df-tru 1378  df-nf 1487  df-sb 1789  df-eu 2060  df-mo 2061  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rex 2494  df-reu 2495  df-rab 2497  df-v 2781  df-sbc 3009  df-csb 3105  df-un 3181  df-in 3183  df-ss 3190  df-pw 3631  df-sn 3652  df-pr 3653  df-op 3655  df-uni 3868  df-iun 3946  df-br 4063  df-opab 4125  df-mpt 4126  df-id 4361  df-xp 4702  df-rel 4703  df-cnv 4704  df-co 4705  df-dm 4706  df-rn 4707  df-res 4708  df-ima 4709  df-iota 5254  df-fun 5296  df-fn 5297  df-f 5298  df-f1 5299  df-fo 5300  df-f1o 5301  df-fv 5302

This theorem is referenced by: (None)