Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Relations and functions (cont.)
oprabexd
Next ⟩
oprabex
Metamath Proof Explorer
Ascii
Unicode
Theorem
oprabexd
Description:
Existence of an operator abstraction.
(Contributed by
Jeff Madsen
, 2-Sep-2009)
Ref
Expression
Hypotheses
oprabexd.1
⊢
φ
→
A
∈
V
oprabexd.2
⊢
φ
→
B
∈
V
oprabexd.3
⊢
φ
∧
x
∈
A
∧
y
∈
B
→
∃
*
z
ψ
oprabexd.4
⊢
φ
→
F
=
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
Assertion
oprabexd
⊢
φ
→
F
∈
V
Proof
Step
Hyp
Ref
Expression
1
oprabexd.1
⊢
φ
→
A
∈
V
2
oprabexd.2
⊢
φ
→
B
∈
V
3
oprabexd.3
⊢
φ
∧
x
∈
A
∧
y
∈
B
→
∃
*
z
ψ
4
oprabexd.4
⊢
φ
→
F
=
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
5
3
ex
⊢
φ
→
x
∈
A
∧
y
∈
B
→
∃
*
z
ψ
6
moanimv
⊢
∃
*
z
x
∈
A
∧
y
∈
B
∧
ψ
↔
x
∈
A
∧
y
∈
B
→
∃
*
z
ψ
7
5
6
sylibr
⊢
φ
→
∃
*
z
x
∈
A
∧
y
∈
B
∧
ψ
8
7
alrimivv
⊢
φ
→
∀
x
∀
y
∃
*
z
x
∈
A
∧
y
∈
B
∧
ψ
9
funoprabg
⊢
∀
x
∀
y
∃
*
z
x
∈
A
∧
y
∈
B
∧
ψ
→
Fun
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
10
8
9
syl
⊢
φ
→
Fun
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
11
dmoprabss
⊢
dom
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
⊆
A
×
B
12
1
2
xpexd
⊢
φ
→
A
×
B
∈
V
13
ssexg
⊢
dom
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
⊆
A
×
B
∧
A
×
B
∈
V
→
dom
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
∈
V
14
11
12
13
sylancr
⊢
φ
→
dom
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
∈
V
15
funex
⊢
Fun
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
∧
dom
⁡
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
∈
V
→
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
∈
V
16
10
14
15
syl2anc
⊢
φ
→
x
y
z
|
x
∈
A
∧
y
∈
B
∧
ψ
∈
V
17
4
16
eqeltrd
⊢
φ
→
F
∈
V