ecxrn

Description: The ( R |X. S ) -coset of A . (Contributed by Peter Mazsa, 18-Apr-2020) (Revised by Peter Mazsa, 21-Sep-2021)

		Ref	Expression
	Assertion	ecxrn	$⊢ A \in V \to [A] R ⋉ S = \{⟨y, z⟩ \| (A R y \land A S z)\}$

Step	Hyp	Ref	Expression
1		elecxrn	$⊢ A \in V \to (x \in [A] R ⋉ S \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land A R y \land A S z))$
2		3anass	$⊢ (x = ⟨y, z⟩ \land A R y \land A S z) \leftrightarrow (x = ⟨y, z⟩ \land (A R y \land A S z))$
3	2	2exbii	$⊢ \exists y \exists z (x = ⟨y, z⟩ \land A R y \land A S z) \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (A R y \land A S z))$
4	1 3	bitrdi	$⊢ A \in V \to (x \in [A] R ⋉ S \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (A R y \land A S z)))$
5		elopab	$⊢ x \in \{⟨y, z⟩ \| (A R y \land A S z)\} \leftrightarrow \exists y \exists z (x = ⟨y, z⟩ \land (A R y \land A S z))$
6	4 5	bitr4di	$⊢ A \in V \to (x \in [A] R ⋉ S \leftrightarrow x \in \{⟨y, z⟩ \| (A R y \land A S z)\})$
7	6	eqrdv	$⊢ A \in V \to [A] R ⋉ S = \{⟨y, z⟩ \| (A R y \land A S z)\}$

Metamath Proof Explorer