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