ecxpid

Description: The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024)

		Ref	Expression
	Assertion	ecxpid	$⊢ X \in A \to [X] (A \times A) = A$

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		elecg	$⊢ (x \in V \land X \in A) \to (x \in [X] (A \times A) \leftrightarrow X (A \times A) x)$
3	1 2	mpan	$⊢ X \in A \to (x \in [X] (A \times A) \leftrightarrow X (A \times A) x)$
4		brxp	$⊢ X (A \times A) x \leftrightarrow (X \in A \land x \in A)$
5	4	baib	$⊢ X \in A \to (X (A \times A) x \leftrightarrow x \in A)$
6	3 5	bitrd	$⊢ X \in A \to (x \in [X] (A \times A) \leftrightarrow x \in A)$
7	6	eqrdv	$⊢ X \in A \to [X] (A \times A) = A$

Metamath Proof Explorer