This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iunsnima

Description: Image of a singleton by an indexed union involving that singleton. (Contributed by Thierry Arnoux, 10-Apr-2020)

Ref Expression
Hypotheses iunsnima.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
iunsnima.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
Assertion iunsnima ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑥 } ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 iunsnima.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 iunsnima.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 3 4 elimasn ⊢ ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
6 opeliunxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
7 6 baib ⊢ ( 𝑥 ∈ 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ 𝑦 ∈ 𝐵 ) )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ 𝑦 ∈ 𝐵 ) )
9 5 8 bitrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑥 } ) ↔ 𝑦 ∈ 𝐵 ) )
10 9 eqrdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑥 } ) = 𝐵 )