Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Equivalence relations and classes
qliftf
Next ⟩
qliftval
Metamath Proof Explorer
Ascii
Unicode
Theorem
qliftf
Description:
The domain and range of the function
F
.
(Contributed by
Mario Carneiro
, 23-Dec-2016)
Ref
Expression
Hypotheses
qlift.1
⊢
F
=
ran
⁡
x
∈
X
⟼
x
R
A
qlift.2
⊢
φ
∧
x
∈
X
→
A
∈
Y
qlift.3
⊢
φ
→
R
Er
X
qlift.4
⊢
φ
→
X
∈
V
Assertion
qliftf
⊢
φ
→
Fun
⁡
F
↔
F
:
X
/
R
⟶
Y
Proof
Step
Hyp
Ref
Expression
1
qlift.1
⊢
F
=
ran
⁡
x
∈
X
⟼
x
R
A
2
qlift.2
⊢
φ
∧
x
∈
X
→
A
∈
Y
3
qlift.3
⊢
φ
→
R
Er
X
4
qlift.4
⊢
φ
→
X
∈
V
5
1
2
3
4
qliftlem
⊢
φ
∧
x
∈
X
→
x
R
∈
X
/
R
6
1
5
2
fliftf
⊢
φ
→
Fun
⁡
F
↔
F
:
ran
⁡
x
∈
X
⟼
x
R
⟶
Y
7
df-qs
⊢
X
/
R
=
y
|
∃
x
∈
X
y
=
x
R
8
eqid
⊢
x
∈
X
⟼
x
R
=
x
∈
X
⟼
x
R
9
8
rnmpt
⊢
ran
⁡
x
∈
X
⟼
x
R
=
y
|
∃
x
∈
X
y
=
x
R
10
7
9
eqtr4i
⊢
X
/
R
=
ran
⁡
x
∈
X
⟼
x
R
11
10
a1i
⊢
φ
→
X
/
R
=
ran
⁡
x
∈
X
⟼
x
R
12
11
feq2d
⊢
φ
→
F
:
X
/
R
⟶
Y
↔
F
:
ran
⁡
x
∈
X
⟼
x
R
⟶
Y
13
6
12
bitr4d
⊢
φ
→
Fun
⁡
F
↔
F
:
X
/
R
⟶
Y