Theorem enfixsn

Description: Given two equipollent sets, a bijection can always be chosen which fixes a single point. (Contributed by Stefan O'Rear, 9-Jul-2015)

	Ref	Expression
Assertion	enfixsn	$$⊢\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\to \exists f\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp3	$$⊢\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\to X\approx Y$$
2		bren	$$⊢X\approx Y\leftrightarrow \exists gg:X\underset{1-1\; onto}{⟶}Y$$
3	1 2	sylib	$$⊢\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\to \exists gg:X\underset{1-1\; onto}{⟶}Y$$
4		relen	$$⊢\mathrm{Rel}\approx$$
5	4	brrelex2i	$$⊢X\approx Y\to Y\in \mathrm{V}$$
6	5	3ad2ant3	$$⊢\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\to Y\in \mathrm{V}$$
7	6	adantr	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to Y\in \mathrm{V}$$
8		f1of	$$⊢g:X\underset{1-1\; onto}{⟶}Y\to g:X⟶Y$$
9	8	adantl	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to g:X⟶Y$$
10		simpl1	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to A\in X$$
11	9 10	ffvelcdmd	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to g\left(A\right)\in Y$$
12		simpl2	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to B\in Y$$
13		difsnen	$$⊢\left(Y\in \mathrm{V}\wedge g\left(A\right)\in Y\wedge B\in Y\right)\to \left(Y\setminus \left\{g\left(A\right)\right\}\right)\approx \left(Y\setminus \left\{B\right\}\right)$$
14	7 11 12 13	syl3anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to \left(Y\setminus \left\{g\left(A\right)\right\}\right)\approx \left(Y\setminus \left\{B\right\}\right)$$
15		bren	$$⊢\left(Y\setminus \left\{g\left(A\right)\right\}\right)\approx \left(Y\setminus \left\{B\right\}\right)\leftrightarrow \exists hh:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}$$
16	14 15	sylib	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to \exists hh:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}$$
17		fvex	$$⊢g\left(A\right)\in \mathrm{V}$$
18	17	a1i	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to g\left(A\right)\in \mathrm{V}$$
19		simpl2	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to B\in Y$$
20		f1osng	$$⊢\left(g\left(A\right)\in \mathrm{V}\wedge B\in Y\right)\to \left\{⟨g\left(A\right),B⟩\right\}:\left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
21	18 19 20	syl2anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left\{⟨g\left(A\right),B⟩\right\}:\left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}$$
22		simprr	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}$$
23		disjdif	$$⊢\left\{g\left(A\right)\right\}\cap \left(Y\setminus \left\{g\left(A\right)\right\}\right)=\varnothing$$
24	23	a1i	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left\{g\left(A\right)\right\}\cap \left(Y\setminus \left\{g\left(A\right)\right\}\right)=\varnothing$$
25		disjdif	$$⊢\left\{B\right\}\cap \left(Y\setminus \left\{B\right\}\right)=\varnothing$$
26	25	a1i	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left\{B\right\}\cap \left(Y\setminus \left\{B\right\}\right)=\varnothing$$
27		f1oun	$$⊢\left(\left(\left\{⟨g\left(A\right),B⟩\right\}:\left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\wedge \left(\left\{g\left(A\right)\right\}\cap \left(Y\setminus \left\{g\left(A\right)\right\}\right)=\varnothing \wedge \left\{B\right\}\cap \left(Y\setminus \left\{B\right\}\right)=\varnothing \right)\right)\to \left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):\left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)\underset{1-1\; onto}{⟶}\left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)$$
28	21 22 24 26 27	syl22anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):\left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)\underset{1-1\; onto}{⟶}\left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)$$
29	8	ad2antrl	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to g:X⟶Y$$
30		simpl1	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to A\in X$$
31	29 30	ffvelcdmd	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to g\left(A\right)\in Y$$
32		uncom	$$⊢\left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)=\left(Y\setminus \left\{g\left(A\right)\right\}\right)\cup \left\{g\left(A\right)\right\}$$
33		difsnid	$$⊢g\left(A\right)\in Y\to \left(Y\setminus \left\{g\left(A\right)\right\}\right)\cup \left\{g\left(A\right)\right\}=Y$$
34	32 33	eqtrid	$$⊢g\left(A\right)\in Y\to \left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)=Y$$
35	31 34	syl	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)=Y$$
36		uncom	$$⊢\left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)=\left(Y\setminus \left\{B\right\}\right)\cup \left\{B\right\}$$
37		difsnid	$$⊢B\in Y\to \left(Y\setminus \left\{B\right\}\right)\cup \left\{B\right\}=Y$$
38	36 37	eqtrid	$$⊢B\in Y\to \left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)=Y$$
39	19 38	syl	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)=Y$$
40		f1oeq23	$$⊢\left(\left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)=Y\wedge \left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)=Y\right)\to \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):\left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)\underset{1-1\; onto}{⟶}\left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)\leftrightarrow \left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):Y\underset{1-1\; onto}{⟶}Y\right)$$
41	35 39 40	syl2anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):\left\{g\left(A\right)\right\}\cup \left(Y\setminus \left\{g\left(A\right)\right\}\right)\underset{1-1\; onto}{⟶}\left\{B\right\}\cup \left(Y\setminus \left\{B\right\}\right)\leftrightarrow \left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):Y\underset{1-1\; onto}{⟶}Y\right)$$
42	28 41	mpbid	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):Y\underset{1-1\; onto}{⟶}Y$$
43		simprl	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to g:X\underset{1-1\; onto}{⟶}Y$$
44		f1oco	$$⊢\left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right):Y\underset{1-1\; onto}{⟶}Y\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right):X\underset{1-1\; onto}{⟶}Y$$
45	42 43 44	syl2anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right):X\underset{1-1\; onto}{⟶}Y$$
46		f1ofn	$$⊢g:X\underset{1-1\; onto}{⟶}Y\to gFnX$$
47	46	ad2antrl	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to gFnX$$
48		fvco2	$$⊢\left(gFnX\wedge A\in X\right)\to \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right)\left(A\right)=\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\left(g\left(A\right)\right)$$
49	47 30 48	syl2anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right)\left(A\right)=\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\left(g\left(A\right)\right)$$
50		f1ofn	$$⊢\left\{⟨g\left(A\right),B⟩\right\}:\left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}\left\{B\right\}\to \left\{⟨g\left(A\right),B⟩\right\}Fn\left\{g\left(A\right)\right\}$$
51	21 50	syl	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left\{⟨g\left(A\right),B⟩\right\}Fn\left\{g\left(A\right)\right\}$$
52		f1ofn	$$⊢h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\to hFn\left(Y\setminus \left\{g\left(A\right)\right\}\right)$$
53	52	ad2antll	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to hFn\left(Y\setminus \left\{g\left(A\right)\right\}\right)$$
54	17	snid	$$⊢g\left(A\right)\in \left\{g\left(A\right)\right\}$$
55	54	a1i	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to g\left(A\right)\in \left\{g\left(A\right)\right\}$$
56		fvun1	$$⊢\left(\left\{⟨g\left(A\right),B⟩\right\}Fn\left\{g\left(A\right)\right\}\wedge hFn\left(Y\setminus \left\{g\left(A\right)\right\}\right)\wedge \left(\left\{g\left(A\right)\right\}\cap \left(Y\setminus \left\{g\left(A\right)\right\}\right)=\varnothing \wedge g\left(A\right)\in \left\{g\left(A\right)\right\}\right)\right)\to \left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\left(g\left(A\right)\right)=\left\{⟨g\left(A\right),B⟩\right\}\left(g\left(A\right)\right)$$
57	51 53 24 55 56	syl112anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\left(g\left(A\right)\right)=\left\{⟨g\left(A\right),B⟩\right\}\left(g\left(A\right)\right)$$
58		fvsng	$$⊢\left(g\left(A\right)\in \mathrm{V}\wedge B\in Y\right)\to \left\{⟨g\left(A\right),B⟩\right\}\left(g\left(A\right)\right)=B$$
59	18 19 58	syl2anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left\{⟨g\left(A\right),B⟩\right\}\left(g\left(A\right)\right)=B$$
60	49 57 59	3eqtrd	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right)\left(A\right)=B$$
61		snex	$$⊢\left\{⟨g\left(A\right),B⟩\right\}\in \mathrm{V}$$
62		vex	$$⊢h\in \mathrm{V}$$
63	61 62	unex	$$⊢\left\{⟨g\left(A\right),B⟩\right\}\cup h\in \mathrm{V}$$
64		vex	$$⊢g\in \mathrm{V}$$
65	63 64	coex	$$⊢\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\in \mathrm{V}$$
66		f1oeq1	$$⊢f=\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\to \left(f:X\underset{1-1\; onto}{⟶}Y\leftrightarrow \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right):X\underset{1-1\; onto}{⟶}Y\right)$$
67		fveq1	$$⊢f=\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\to f\left(A\right)=\left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right)\left(A\right)$$
68	67	eqeq1d	$$⊢f=\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\to \left(f\left(A\right)=B\leftrightarrow \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right)\left(A\right)=B\right)$$
69	66 68	anbi12d	$$⊢f=\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\to \left(\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)\leftrightarrow \left(\left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right):X\underset{1-1\; onto}{⟶}Y\wedge \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right)\left(A\right)=B\right)\right)$$
70	65 69	spcev	$$⊢\left(\left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right):X\underset{1-1\; onto}{⟶}Y\wedge \left(\left(\left\{⟨g\left(A\right),B⟩\right\}\cup h\right)\circ g\right)\left(A\right)=B\right)\to \exists f\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)$$
71	45 60 70	syl2anc	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge \left(g:X\underset{1-1\; onto}{⟶}Y\wedge h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\right)\right)\to \exists f\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)$$
72	71	expr	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to \left(h:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\to \exists f\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)\right)$$
73	72	exlimdv	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to \left(\exists hh:Y\setminus \left\{g\left(A\right)\right\}\underset{1-1\; onto}{⟶}Y\setminus \left\{B\right\}\to \exists f\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)\right)$$
74	16 73	mpd	$$⊢\left(\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\wedge g:X\underset{1-1\; onto}{⟶}Y\right)\to \exists f\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)$$
75	3 74	exlimddv	$$⊢\left(A\in X\wedge B\in Y\wedge X\approx Y\right)\to \exists f\left(f:X\underset{1-1\; onto}{⟶}Y\wedge f\left(A\right)=B\right)$$