Metamath Proof Explorer


Theorem ac6gf

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

Ref Expression
Hypotheses ac6gf.1 y ψ
ac6gf.2 y = f x φ ψ
Assertion ac6gf A C x A y B φ f f : A B x A ψ

Proof

Step Hyp Ref Expression
1 ac6gf.1 y ψ
2 ac6gf.2 y = f x φ ψ
3 cbvrexsvw y B φ z B z y φ
4 3 ralbii x A y B φ x A z B z y φ
5 1 2 sbhypf z = f x z y φ ψ
6 5 ac6sg A C x A z B z y φ f f : A B x A ψ
7 6 imp A C x A z B z y φ f f : A B x A ψ
8 4 7 sylan2b A C x A y B φ f f : A B x A ψ