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