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	⊢ ( ( 𝜑 ∧ 𝑌 ∈ 𝐴 ) → ( ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) “ { 𝑌 } ) = 𝐶 )