Theorem ac6num

Description: A version of ac6 which takes the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

	Ref	Expression
Hypothesis	ac6num.1	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6num	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ac6num.1	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
2		nfiu1	$$⊢\underset{\_}{Ⅎ}x\bigcup _{x\in A}\left\{y\in B|\phi \right\}$$
3	2	nfel1	$$⊢Ⅎx\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}$$
4		ssiun2	$$⊢x\in A\to \left\{y\in B|\phi \right\}\subseteq \bigcup _{x\in A}\left\{y\in B|\phi \right\}$$
5		ssexg	$$⊢\left(\left\{y\in B|\phi \right\}\subseteq \bigcup _{x\in A}\left\{y\in B|\phi \right\}\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\right)\to \left\{y\in B|\phi \right\}\in \mathrm{V}$$
6	5	expcom	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \left(\left\{y\in B|\phi \right\}\subseteq \bigcup _{x\in A}\left\{y\in B|\phi \right\}\to \left\{y\in B|\phi \right\}\in \mathrm{V}\right)$$
7	4 6	syl5	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \left(x\in A\to \left\{y\in B|\phi \right\}\in \mathrm{V}\right)$$
8	3 7	ralrimi	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}$$
9		dfiun2g	$$⊢\forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}=\bigcup \left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
10	8 9	syl	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}=\bigcup \left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
11		eqid	$$⊢\left(x\in A⟼\left\{y\in B|\phi \right\}\right)=\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
12	11	rnmpt	$$⊢\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)=\left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
13	12	unieqi	$$⊢\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)=\bigcup \left\{z|\exists x\in Az=\left\{y\in B|\phi \right\}\right\}$$
14	10 13	eqtr4di	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}=\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
15		id	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}$$
16	14 15	eqeltrrd	$$⊢\bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\to \bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\in \mathrm{dom}\mathrm{card}$$
17	16	3ad2ant2	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\in \mathrm{dom}\mathrm{card}$$
18		simp3	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \forall x\in A\exists y\in B\phi$$
19		necom	$$⊢\left\{y\in B|\phi \right\}\ne \varnothing \leftrightarrow \varnothing \ne \left\{y\in B|\phi \right\}$$
20		rabn0	$$⊢\left\{y\in B|\phi \right\}\ne \varnothing \leftrightarrow \exists y\in B\phi$$
21		df-ne	$$⊢\varnothing \ne \left\{y\in B|\phi \right\}\leftrightarrow \neg \varnothing =\left\{y\in B|\phi \right\}$$
22	19 20 21	3bitr3i	$$⊢\exists y\in B\phi \leftrightarrow \neg \varnothing =\left\{y\in B|\phi \right\}$$
23	22	ralbii	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \forall x\in A\neg \varnothing =\left\{y\in B|\phi \right\}$$
24		ralnex	$$⊢\forall x\in A\neg \varnothing =\left\{y\in B|\phi \right\}\leftrightarrow \neg \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
25	23 24	bitri	$$⊢\forall x\in A\exists y\in B\phi \leftrightarrow \neg \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
26	18 25	sylib	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \neg \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
27		0ex	$$⊢\varnothing \in \mathrm{V}$$
28	11	elrnmpt	$$⊢\varnothing \in \mathrm{V}\to \left(\varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\leftrightarrow \exists x\in A\varnothing =\left\{y\in B|\phi \right\}\right)$$
29	27 28	ax-mp	$$⊢\varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\leftrightarrow \exists x\in A\varnothing =\left\{y\in B|\phi \right\}$$
30	26 29	sylnibr	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \neg \varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
31		ac5num	$$⊢\left(\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\in \mathrm{dom}\mathrm{card}\wedge \neg \varnothing \in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\right)\to \exists g\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)$$
32	17 30 31	syl2anc	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists g\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)$$
33		ffn	$$⊢g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\to gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)$$
34	33	anim1i	$$⊢\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)$$
35	8	3ad2ant2	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}$$
36		fveq2	$$⊢z=\left\{y\in B|\phi \right\}\to g\left(z\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
37		id	$$⊢z=\left\{y\in B|\phi \right\}\to z=\left\{y\in B|\phi \right\}$$
38	36 37	eleq12d	$$⊢z=\left\{y\in B|\phi \right\}\to \left(g\left(z\right)\in z\leftrightarrow g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)$$
39	11 38	ralrnmptw	$$⊢\forall x\in A\left\{y\in B|\phi \right\}\in \mathrm{V}\to \left(\forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\leftrightarrow \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)$$
40	35 39	syl	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\leftrightarrow \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)$$
41	40	anbi2d	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\leftrightarrow \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)$$
42	34 41	syl5ib	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)$$
43		simpl1	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to A\in V$$
44	43	mptexd	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\in \mathrm{V}$$
45		ssrab2	$$⊢\left\{y\in B|\phi \right\}\subseteq B$$
46	45	sseli	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to g\left(\left\{y\in B|\phi \right\}\right)\in B$$
47	46	ralimi	$$⊢\forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in B$$
48	47	ad2antll	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in B$$
49		eqid	$$⊢\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)$$
50	49	fmpt	$$⊢\forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in B\leftrightarrow \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B$$
51	48 50	sylib	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B$$
52		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
53	52	elrabsf	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\leftrightarrow \left(g\left(\left\{y\in B|\phi \right\}\right)\in B\wedge \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
54	53	simprbi	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi$$
55	54	ralimi	$$⊢\forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\to \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi$$
56	55	ad2antll	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi$$
57	51 56	jca	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \left(\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B\wedge \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
58		feq1	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to \left(f:A⟶B\leftrightarrow \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B\right)$$
59		nfmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)$$
60	59	nfeq2	$$⊢Ⅎxf=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)$$
61		fvex	$$⊢f\left(x\right)\in \mathrm{V}$$
62	61 1	sbcie	$$⊢\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
63		fveq1	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to f\left(x\right)=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\left(x\right)$$
64		fvex	$$⊢g\left(\left\{y\in B|\phi \right\}\right)\in \mathrm{V}$$
65	49	fvmpt2	$$⊢\left(x\in A\wedge g\left(\left\{y\in B|\phi \right\}\right)\in \mathrm{V}\right)\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\left(x\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
66	64 65	mpan2	$$⊢x\in A\to \left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\left(x\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
67	63 66	sylan9eq	$$⊢\left(f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\wedge x\in A\right)\to f\left(x\right)=g\left(\left\{y\in B|\phi \right\}\right)$$
68	67	sbceq1d	$$⊢\left(f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\wedge x\in A\right)\to \left(\underset{\dot{}}{[}f\left(x\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
69	62 68	bitr3id	$$⊢\left(f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\wedge x\in A\right)\to \left(\psi \leftrightarrow \underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
70	60 69	ralbida	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to \left(\forall x\in A\psi \leftrightarrow \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)$$
71	58 70	anbi12d	$$⊢f=\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right)\to \left(\left(f:A⟶B\wedge \forall x\in A\psi \right)\leftrightarrow \left(\left(x\in A⟼g\left(\left\{y\in B|\phi \right\}\right)\right):A⟶B\wedge \forall x\in A\underset{\dot{}}{[}g\left(\left\{y\in B|\phi \right\}\right)/y\underset{\dot{}}{]}\phi \right)\right)$$
72	44 57 71	spcedv	$$⊢\left(\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\wedge \left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$
73	72	ex	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(gFn\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall x\in Ag\left(\left\{y\in B|\phi \right\}\right)\in \left\{y\in B|\phi \right\}\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)\right)$$
74	42 73	syld	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)\right)$$
75	74	exlimdv	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \left(\exists g\left(g:\mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)⟶\bigcup \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)\wedge \forall z\in \mathrm{ran}\left(x\in A⟼\left\{y\in B|\phi \right\}\right)g\left(z\right)\in z\right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)\right)$$
76	32 75	mpd	$$⊢\left(A\in V\wedge \bigcup _{x\in A}\left\{y\in B|\phi \right\}\in \mathrm{dom}\mathrm{card}\wedge \forall x\in A\exists y\in B\phi \right)\to \exists f\left(f:A⟶B\wedge \forall x\in A\psi \right)$$