Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Operations
elimampo
Next ⟩
elrnmpores
Metamath Proof Explorer
Ascii
Unicode
Theorem
elimampo
Description:
Membership in the image of an operation.
(Contributed by
SN
, 27-Apr-2025)
Ref
Expression
Hypotheses
rngop.1
⊢
F
=
x
∈
A
,
y
∈
B
⟼
C
elimampo.d
⊢
φ
→
D
∈
V
elimampo.x
⊢
φ
→
X
⊆
A
elimampo.y
⊢
φ
→
Y
⊆
B
Assertion
elimampo
⊢
φ
→
D
∈
F
X
×
Y
↔
∃
x
∈
X
∃
y
∈
Y
D
=
C
Proof
Step
Hyp
Ref
Expression
1
rngop.1
⊢
F
=
x
∈
A
,
y
∈
B
⟼
C
2
elimampo.d
⊢
φ
→
D
∈
V
3
elimampo.x
⊢
φ
→
X
⊆
A
4
elimampo.y
⊢
φ
→
Y
⊆
B
5
df-ima
⊢
F
X
×
Y
=
ran
⁡
F
↾
X
×
Y
6
5
eleq2i
⊢
D
∈
F
X
×
Y
↔
D
∈
ran
⁡
F
↾
X
×
Y
7
1
reseq1i
⊢
F
↾
X
×
Y
=
x
∈
A
,
y
∈
B
⟼
C
↾
X
×
Y
8
resmpo
⊢
X
⊆
A
∧
Y
⊆
B
→
x
∈
A
,
y
∈
B
⟼
C
↾
X
×
Y
=
x
∈
X
,
y
∈
Y
⟼
C
9
3
4
8
syl2anc
⊢
φ
→
x
∈
A
,
y
∈
B
⟼
C
↾
X
×
Y
=
x
∈
X
,
y
∈
Y
⟼
C
10
7
9
eqtrid
⊢
φ
→
F
↾
X
×
Y
=
x
∈
X
,
y
∈
Y
⟼
C
11
10
rneqd
⊢
φ
→
ran
⁡
F
↾
X
×
Y
=
ran
⁡
x
∈
X
,
y
∈
Y
⟼
C
12
11
eleq2d
⊢
φ
→
D
∈
ran
⁡
F
↾
X
×
Y
↔
D
∈
ran
⁡
x
∈
X
,
y
∈
Y
⟼
C
13
6
12
bitrid
⊢
φ
→
D
∈
F
X
×
Y
↔
D
∈
ran
⁡
x
∈
X
,
y
∈
Y
⟼
C
14
eqid
⊢
x
∈
X
,
y
∈
Y
⟼
C
=
x
∈
X
,
y
∈
Y
⟼
C
15
14
elrnmpog
⊢
D
∈
V
→
D
∈
ran
⁡
x
∈
X
,
y
∈
Y
⟼
C
↔
∃
x
∈
X
∃
y
∈
Y
D
=
C
16
2
15
syl
⊢
φ
→
D
∈
ran
⁡
x
∈
X
,
y
∈
Y
⟼
C
↔
∃
x
∈
X
∃
y
∈
Y
D
=
C
17
13
16
bitrd
⊢
φ
→
D
∈
F
X
×
Y
↔
∃
x
∈
X
∃
y
∈
Y
D
=
C