iunsnima

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

Step	Hyp	Ref	Expression
1		iunsnima.1	$⊢ φ \to A \in V$
2		iunsnima.2	$⊢ (φ \land x \in A) \to B \in W$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	elimasn	$⊢ y \in ⋃_{x \in A} (\{x\} \times B) [\{x\}] \leftrightarrow ⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B)$
6		opeliunxp	$⊢ ⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow (x \in A \land y \in B)$
7	6	baib	$⊢ x \in A \to (⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow y \in B)$
8	7	adantl	$⊢ (φ \land x \in A) \to (⟨x, y⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow y \in B)$
9	5 8	bitrid	$⊢ (φ \land x \in A) \to (y \in ⋃_{x \in A} (\{x\} \times B) [\{x\}] \leftrightarrow y \in B)$
10	9	eqrdv	$⊢ (φ \land x \in A) \to ⋃_{x \in A} (\{x\} \times B) [\{x\}] = B$

Metamath Proof Explorer