Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Function operation
nfof
Next ⟩
nfofr
Metamath Proof Explorer
Ascii
Unicode
Theorem
nfof
Description:
Hypothesis builder for function operation.
(Contributed by
Mario Carneiro
, 20-Jul-2014)
Ref
Expression
Hypothesis
nfof.1
⊢
Ⅎ
_
x
R
Assertion
nfof
⊢
Ⅎ
_
x
∘
f
⁡
R
Proof
Step
Hyp
Ref
Expression
1
nfof.1
⊢
Ⅎ
_
x
R
2
df-of
⊢
∘
f
⁡
R
=
u
∈
V
,
v
∈
V
⟼
w
∈
dom
⁡
u
∩
dom
⁡
v
⟼
u
⁡
w
R
v
⁡
w
3
nfcv
⊢
Ⅎ
_
x
V
4
nfcv
⊢
Ⅎ
_
x
dom
⁡
u
∩
dom
⁡
v
5
nfcv
⊢
Ⅎ
_
x
u
⁡
w
6
nfcv
⊢
Ⅎ
_
x
v
⁡
w
7
5
1
6
nfov
⊢
Ⅎ
_
x
u
⁡
w
R
v
⁡
w
8
4
7
nfmpt
⊢
Ⅎ
_
x
w
∈
dom
⁡
u
∩
dom
⁡
v
⟼
u
⁡
w
R
v
⁡
w
9
3
3
8
nfmpo
⊢
Ⅎ
_
x
u
∈
V
,
v
∈
V
⟼
w
∈
dom
⁡
u
∩
dom
⁡
v
⟼
u
⁡
w
R
v
⁡
w
10
2
9
nfcxfr
⊢
Ⅎ
_
x
∘
f
⁡
R