# Metamath Proof Explorer

## 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 }↔{\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 ac6num.1 ${⊢}{y}={f}\left({x}\right)\to \left({\phi }↔{\psi }\right)$
2 nfiu1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\bigcup _{{x}\in {A}}\left\{{y}\in {B}|{\phi }\right\}$
3 2 nfel1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\left\{{y}\in {B}|{\phi }\right\}\in \mathrm{V}$
9 dfiun2g ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\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 {A}\phantom{\rule{.4em}{0ex}}{z}=\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 {A}\phantom{\rule{.4em}{0ex}}{z}=\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 {A}\phantom{\rule{.4em}{0ex}}{z}=\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 {A}\phantom{\rule{.4em}{0ex}}{z}=\left\{{y}\in {B}|{\phi }\right\}\right\}$
14 10 13 syl6eqr ${⊢}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
19 necom ${⊢}\left\{{y}\in {B}|{\phi }\right\}\ne \varnothing ↔\varnothing \ne \left\{{y}\in {B}|{\phi }\right\}$
20 rabn0 ${⊢}\left\{{y}\in {B}|{\phi }\right\}\ne \varnothing ↔\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }$
21 df-ne ${⊢}\varnothing \ne \left\{{y}\in {B}|{\phi }\right\}↔¬\varnothing =\left\{{y}\in {B}|{\phi }\right\}$
22 19 20 21 3bitr3i ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\varnothing =\left\{{y}\in {B}|{\phi }\right\}$
23 22 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\varnothing =\left\{{y}\in {B}|{\phi }\right\}$
24 ralnex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬\varnothing =\left\{{y}\in {B}|{\phi }\right\}↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\varnothing =\left\{{y}\in {B}|{\phi }\right\}$
25 23 24 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to ¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\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)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\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)↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to ¬\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 ¬\varnothing \in \mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}{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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}{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 {g}Fn\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)\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in {z}\right)\to \left({g}Fn\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)\phantom{\rule{.4em}{0ex}}{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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\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}↔{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}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in {z}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\forall {z}\in \mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in {z}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({g}Fn\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)\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in {z}\right)↔\left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\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)\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in {z}\right)\to \left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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 {A}\phantom{\rule{.4em}{0ex}}{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\in \left\{{y}\in {B}|{\phi }\right\}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\in \left\{{y}\in {B}|{\phi }\right\}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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 {A}\phantom{\rule{.4em}{0ex}}{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\in {B}↔\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\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{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
53 52 elrabsf
54 53 simprbi
55 54 ralimi
57 51 56 jca
58 feq1 ${⊢}{f}=\left({x}\in {A}⟼{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\right)\to \left({f}:{A}⟶{B}↔\left({x}\in {A}⟼{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\right):{A}⟶{B}\right)$
59 nfmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\right)$
60 59 nfeq2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{f}=\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
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
69 62 68 syl5bbr
70 60 69 ralbida
71 58 70 anbi12d
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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\wedge \left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\in \left\{{y}\in {B}|{\phi }\right\}\right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\left({g}Fn\mathrm{ran}\left({x}\in {A}⟼\left\{{y}\in {B}|{\phi }\right\}\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left(\left\{{y}\in {B}|{\phi }\right\}\right)\in \left\{{y}\in {B}|{\phi }\right\}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\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)\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in {z}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \left(\exists {g}\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}{g}\left({z}\right)\in {z}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\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}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$