ecun

Description: The union coset of A . (Contributed by Peter Mazsa, 28-Jan-2026)

		Ref	Expression
	Assertion	ecun	$⊢ A \in V \to [A] (R \cup S) = [A] R \cup [A] S$

Step	Hyp	Ref	Expression
1		unab	$⊢ \{x \| A R x\} \cup \{x \| A S x\} = \{x \| (A R x \lor A S x)\}$
2	1	a1i	$⊢ A \in V \to \{x \| A R x\} \cup \{x \| A S x\} = \{x \| (A R x \lor A S x)\}$
3		dfec2	$⊢ A \in V \to [A] R = \{x \| A R x\}$
4		dfec2	$⊢ A \in V \to [A] S = \{x \| A S x\}$
5	3 4	uneq12d	$⊢ A \in V \to [A] R \cup [A] S = \{x \| A R x\} \cup \{x \| A S x\}$
6		elecALTV	$⊢ (A \in V \land x \in V) \to (x \in [A] (R \cup S) \leftrightarrow A (R \cup S) x)$
7	6	elvd	$⊢ A \in V \to (x \in [A] (R \cup S) \leftrightarrow A (R \cup S) x)$
8		brun	$⊢ A (R \cup S) x \leftrightarrow (A R x \lor A S x)$
9	7 8	bitrdi	$⊢ A \in V \to (x \in [A] (R \cup S) \leftrightarrow (A R x \lor A S x))$
10	9	eqabdv	$⊢ A \in V \to [A] (R \cup S) = \{x \| (A R x \lor A S x)\}$
11	2 5 10	3eqtr4rd	$⊢ A \in V \to [A] (R \cup S) = [A] R \cup [A] S$

Metamath Proof Explorer