Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Indexed union and intersection
iineq2dv
Next ⟩
iuneq12df
Metamath Proof Explorer
Ascii
Unicode
Theorem
iineq2dv
Description:
Equality deduction for indexed intersection.
(Contributed by
NM
, 3-Aug-2004)
Ref
Expression
Hypothesis
iuneq2dv.1
⊢
φ
∧
x
∈
A
→
B
=
C
Assertion
iineq2dv
⊢
φ
→
⋂
x
∈
A
B
=
⋂
x
∈
A
C
Proof
Step
Hyp
Ref
Expression
1
iuneq2dv.1
⊢
φ
∧
x
∈
A
→
B
=
C
2
1
ralrimiva
⊢
φ
→
∀
x
∈
A
B
=
C
3
iineq2
⊢
∀
x
∈
A
B
=
C
→
⋂
x
∈
A
B
=
⋂
x
∈
A
C
4
2
3
syl
⊢
φ
→
⋂
x
∈
A
B
=
⋂
x
∈
A
C