Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Brendan Leahy
rabiun
Next ⟩
iundif1
Metamath Proof Explorer
Ascii
Unicode
Theorem
rabiun
Description:
Abstraction restricted to an indexed union.
(Contributed by
Brendan Leahy
, 26-Oct-2017)
Ref
Expression
Assertion
rabiun
⊢
x
∈
⋃
y
∈
A
B
|
φ
=
⋃
y
∈
A
x
∈
B
|
φ
Proof
Step
Hyp
Ref
Expression
1
eliun
⊢
x
∈
⋃
y
∈
A
B
↔
∃
y
∈
A
x
∈
B
2
1
anbi1i
⊢
x
∈
⋃
y
∈
A
B
∧
φ
↔
∃
y
∈
A
x
∈
B
∧
φ
3
r19.41v
⊢
∃
y
∈
A
x
∈
B
∧
φ
↔
∃
y
∈
A
x
∈
B
∧
φ
4
2
3
bitr4i
⊢
x
∈
⋃
y
∈
A
B
∧
φ
↔
∃
y
∈
A
x
∈
B
∧
φ
5
4
abbii
⊢
x
|
x
∈
⋃
y
∈
A
B
∧
φ
=
x
|
∃
y
∈
A
x
∈
B
∧
φ
6
df-rab
⊢
x
∈
⋃
y
∈
A
B
|
φ
=
x
|
x
∈
⋃
y
∈
A
B
∧
φ
7
iunab
⊢
⋃
y
∈
A
x
|
x
∈
B
∧
φ
=
x
|
∃
y
∈
A
x
∈
B
∧
φ
8
5
6
7
3eqtr4i
⊢
x
∈
⋃
y
∈
A
B
|
φ
=
⋃
y
∈
A
x
|
x
∈
B
∧
φ
9
df-rab
⊢
x
∈
B
|
φ
=
x
|
x
∈
B
∧
φ
10
9
a1i
⊢
y
∈
A
→
x
∈
B
|
φ
=
x
|
x
∈
B
∧
φ
11
10
iuneq2i
⊢
⋃
y
∈
A
x
∈
B
|
φ
=
⋃
y
∈
A
x
|
x
∈
B
∧
φ
12
8
11
eqtr4i
⊢
x
∈
⋃
y
∈
A
B
|
φ
=
⋃
y
∈
A
x
∈
B
|
φ