Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Miscellanea
iuneq1i
Next ⟩
nssrex
Metamath Proof Explorer
Ascii
Unicode
Theorem
iuneq1i
Description:
Equality theorem for indexed union.
(Contributed by
Glauco Siliprandi
, 3-Mar-2021)
Ref
Expression
Hypothesis
iuneq1i.1
⊢
A
=
B
Assertion
iuneq1i
⊢
⋃
x
∈
A
C
=
⋃
x
∈
B
C
Proof
Step
Hyp
Ref
Expression
1
iuneq1i.1
⊢
A
=
B
2
iuneq1
⊢
A
=
B
→
⋃
x
∈
A
C
=
⋃
x
∈
B
C
3
1
2
ax-mp
⊢
⋃
x
∈
A
C
=
⋃
x
∈
B
C