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

Metamath Proof Explorer

Theorem iunsnima2

Description: Version of iunsnima with different variables. (Contributed by Thierry Arnoux, 22-Jun-2024)

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

Proof

Step Hyp Ref Expression
1 iunsnima.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 iunsnima.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
3 iunsnima2.1 ⊢ Ⅎ 𝑥 𝐶
4 iunsnima2.2 ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐶 )
5 elimasng ⊢ ( ( 𝑌 ∈ 𝐴 ∧ 𝑧 ∈ V ) → ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑌 } ) ↔ ⟨ 𝑌 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
6 5 elvd ⊢ ( 𝑌 ∈ 𝐴 → ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑌 } ) ↔ ⟨ 𝑌 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
7 6 adantl ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑌 } ) ↔ ⟨ 𝑌 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
8 3 4 opeliunxp2f ⊢ ( ⟨ 𝑌 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑌 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) )
9 8 baib ⊢ ( 𝑌 ∈ 𝐴 → ( ⟨ 𝑌 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ 𝑧 ∈ 𝐶 ) )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( ⟨ 𝑌 , 𝑧 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ 𝑧 ∈ 𝐶 ) )
11 7 10 bitrd ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑧 ∈ ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑌 } ) ↔ 𝑧 ∈ 𝐶 ) )
12 11 eqrdv ⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑌 } ) = 𝐶 )