Metamath Proof Explorer


Theorem ac6s3

Description: Generalization of the Axiom of Choice to classes. Theorem 10.46 of TakeutiZaring p. 97. (Contributed by NM, 3-Nov-2004)

Ref Expression
Hypotheses ac6s.1 A V
ac6s.2 y = f x φ ψ
Assertion ac6s3 x A y φ f x A ψ

Proof

Step Hyp Ref Expression
1 ac6s.1 A V
2 ac6s.2 y = f x φ ψ
3 1 2 ac6s2 x A y φ f f Fn A x A ψ
4 exsimpr f f Fn A x A ψ f x A ψ
5 3 4 syl x A y φ f x A ψ