Metamath Proof Explorer


Theorem iinconst

Description: Indexed intersection of a constant class, i.e. where B does not depend on x . (Contributed by Mario Carneiro, 6-Feb-2015)

Ref Expression
Assertion iinconst ( 𝐴 ≠ ∅ → 𝑥𝐴 𝐵 = 𝐵 )

Proof

Step Hyp Ref Expression
1 r19.3rzv ( 𝐴 ≠ ∅ → ( 𝑦𝐵 ↔ ∀ 𝑥𝐴 𝑦𝐵 ) )
2 eliin ( 𝑦 ∈ V → ( 𝑦 𝑥𝐴 𝐵 ↔ ∀ 𝑥𝐴 𝑦𝐵 ) )
3 2 elv ( 𝑦 𝑥𝐴 𝐵 ↔ ∀ 𝑥𝐴 𝑦𝐵 )
4 1 3 syl6rbbr ( 𝐴 ≠ ∅ → ( 𝑦 𝑥𝐴 𝐵𝑦𝐵 ) )
5 4 eqrdv ( 𝐴 ≠ ∅ → 𝑥𝐴 𝐵 = 𝐵 )