Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
elrn2
Next ⟩
elrn
Metamath Proof Explorer
Ascii
Unicode
Theorem
elrn2
Description:
Membership in a range.
(Contributed by
NM
, 10-Jul-1994)
Ref
Expression
Hypothesis
elrn.1
⊢
A
∈
V
Assertion
elrn2
⊢
A
∈
ran
⁡
B
↔
∃
x
x
A
∈
B
Proof
Step
Hyp
Ref
Expression
1
elrn.1
⊢
A
∈
V
2
opeq2
⊢
y
=
A
→
x
y
=
x
A
3
2
eleq1d
⊢
y
=
A
→
x
y
∈
B
↔
x
A
∈
B
4
3
exbidv
⊢
y
=
A
→
∃
x
x
y
∈
B
↔
∃
x
x
A
∈
B
5
dfrn3
⊢
ran
⁡
B
=
y
|
∃
x
x
y
∈
B
6
1
4
5
elab2
⊢
A
∈
ran
⁡
B
↔
∃
x
x
A
∈
B