Metamath Proof Explorer

Theorem ac6gf

Description: Axiom of Choice. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses ac6gf.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
ac6gf.2 ${⊢}{y}={f}\left({x}\right)\to \left({\phi }↔{\psi }\right)$
Assertion ac6gf ${⊢}\left({A}\in {C}\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 ac6gf.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\psi }$
2 ac6gf.2 ${⊢}{y}={f}\left({x}\right)\to \left({\phi }↔{\psi }\right)$
3 cbvrexsvw ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }$
4 3 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}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }$
5 1 2 sbhypf ${⊢}{z}={f}\left({x}\right)\to \left(\left[{z}/{y}\right]{\phi }↔{\psi }\right)$
6 5 ac6sg ${⊢}{A}\in {C}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)\right)$
7 6 imp ${⊢}\left({A}\in {C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {z}\in {B}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\left({f}:{A}⟶{B}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }\right)$
8 4 7 sylan2b ${⊢}\left({A}\in {C}\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)$