Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jeff Madsen
Logic and set theory
ac6gf
Next ⟩
indexa
Metamath Proof Explorer
Ascii
Unicode
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
ψ