Theorem uchoice 6295

Description: Principle of unique choice. This is also called non-choice. The name choice results in its similarity to something like acfun 7415 (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 2229	. . . . . . . . 9 |- { <. x , y >. | ( x e. A /\ ph ) } = { <. x , y >. | ( x e. A /\ ph ) }
2	1	fnopabg 5453	. . . . . . . 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 5871	. . . . . 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 5681	. . . . . . . . . 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 1574	. . . . . . . . . . . 12 |- F/ x u e. A
10		nfsbc1v 3048	. . . . . . . . . . . 12 |- F/ x [. u / x ]. ph
11	9, 10	nfan 1611	. . . . . . . . . . 11 |- F/ x ( u e. A /\ [. u / x ]. ph )
12		nfv 1574	. . . . . . . . . . . 12 |- F/ y u e. A
13		nfsbc1v 3048	. . . . . . . . . . . 12 |- F/ y [. v / y ]. [. u / x ]. ph
14	12, 13	nfan 1611	. . . . . . . . . . 11 |- F/ y ( u e. A /\ [. v / y ]. [. u / x ]. ph )
15		vex 2803	. . . . . . . . . . 11 |- u e. _V
16		vex 2803	. . . . . . . . . . 11 |- v e. _V
17		eleq1w 2290	. . . . . . . . . . . 12 |- ( x = u -> ( x e. A <-> u e. A ) )
18		sbceq1a 3039	. . . . . . . . . . . 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 3039	. . . . . . . . . . . 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 4367	. . . . . . . . . 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 2603	. . . . . . . 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 1920	. . . . . . 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 5415	. . . . . 6 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( f Fn A <-> { <. x , y >. | ( x e. A /\ ph ) } Fn A ) )
29		fveq1 5634	. . . . . . . . . 10 |- ( f = { <. x , y >. | ( x e. A /\ ph ) } -> ( f ` u ) = ( { <. x , y >. | ( x e. A /\ ph ) } ` u ) )
30	29	eqeq1d 2238	. . . . . . . . 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 2530	. . . . . . 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 1870	. . . . . 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 2949	. . . 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 2823	. . . . . 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 1651	. . . 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 1574	. . . . . . . 8 |- F/ x ( f ` u ) = v
41		nfcv 2372	. . . . . . . . . 10 |- F/_ x v
42	41, 10	nfsbc 3050	. . . . . . . . 9 |- F/ x [. v / y ]. [. u / x ]. ph
43	9, 42	nfan 1611	. . . . . . . 8 |- F/ x ( u e. A /\ [. v / y ]. [. u / x ]. ph )
44	40, 43	nfbi 1635	. . . . . . 7 |- F/ x ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) )
45	44	nfal 1622	. . . . . 6 |- F/ x A. v ( ( f ` u ) = v <-> ( u e. A /\ [. v / y ]. [. u / x ]. ph ) )
46		nfv 1574	. . . . . 6 |- F/ u A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) )
47		fveqeq2 5644	. . . . . . . 8 |- ( u = x -> ( ( f ` u ) = v <-> ( f ` x ) = v ) )
48		eleq1w 2290	. . . . . . . . 9 |- ( u = x -> ( u e. A <-> x e. A ) )
49		sbceq2a 3040	. . . . . . . . . 10 |- ( u = x -> ( [. u / x ]. ph <-> ph ) )
50	49	sbcbidv 3088	. . . . . . . . 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 1870	. . . . . 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 2761	. . . . 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 1651	. . 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 2230	. . . . . . 7 |- ( A. v ( ( f ` x ) = v <-> ( x e. A /\ [. v / y ]. ph ) ) -> ( f ` x ) = ( f ` x ) )
59		vex 2803	. . . . . . . . 9 |- f e. _V
60		vex 2803	. . . . . . . . 9 |- x e. _V
61	59, 60	fvex 5655	. . . . . . . 8 |- ( f ` x ) e. _V
62		eqeq2 2239	. . . . . . . . 9 |- ( v = ( f ` x ) -> ( ( f ` x ) = v <-> ( f ` x ) = ( f ` x ) ) )
63		dfsbcq 3031	. . . . . . . . . 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 2898	. . . . . . 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 2593	. . . 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 1646	. 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 1393   = wceq 1395   E.wex 1538   E!weu 2077   e. wcel 2200   A.wral 2508   _Vcvv 2800   [.wsbc 3029   <.cop 3670   {copab 4147   Fn wfn 5319   ` cfv 5324

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4202  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-iun 3970  df-br 4087  df-opab 4149  df-mpt 4150  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-fv 5332

This theorem is referenced by: (None)