iunsnima2

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

Step	Hyp	Ref	Expression
1		iunsnima.1	$⊢ φ \to A \in V$
2		iunsnima.2	$⊢ (φ \land x \in A) \to B \in W$
3		iunsnima2.1	$⊢ \underline{Ⅎ} x C$
4		iunsnima2.2	$⊢ x = Y \to B = C$
5		elimasng	$⊢ (Y \in A \land z \in V) \to (z \in ⋃_{x \in A} (\{x\} \times B) [\{Y\}] \leftrightarrow ⟨Y, z⟩ \in ⋃_{x \in A} (\{x\} \times B))$
6	5	elvd	$⊢ Y \in A \to (z \in ⋃_{x \in A} (\{x\} \times B) [\{Y\}] \leftrightarrow ⟨Y, z⟩ \in ⋃_{x \in A} (\{x\} \times B))$
7	6	adantl	$⊢ (φ \land Y \in A) \to (z \in ⋃_{x \in A} (\{x\} \times B) [\{Y\}] \leftrightarrow ⟨Y, z⟩ \in ⋃_{x \in A} (\{x\} \times B))$
8	3 4	opeliunxp2f	$⊢ ⟨Y, z⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow (Y \in A \land z \in C)$
9	8	baib	$⊢ Y \in A \to (⟨Y, z⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow z \in C)$
10	9	adantl	$⊢ (φ \land Y \in A) \to (⟨Y, z⟩ \in ⋃_{x \in A} (\{x\} \times B) \leftrightarrow z \in C)$
11	7 10	bitrd	$⊢ (φ \land Y \in A) \to (z \in ⋃_{x \in A} (\{x\} \times B) [\{Y\}] \leftrightarrow z \in C)$
12	11	eqrdv	$⊢ (φ \land Y \in A) \to ⋃_{x \in A} (\{x\} \times B) [\{Y\}] = C$

Metamath Proof Explorer