Theorem 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 e. A -> [ X ] ( A X. A ) = A )

Proof

Step	Hyp	Ref	Expression
1		vex	|- x e. _V
2		elecg	|- ( ( x e. _V /\ X e. A ) -> ( x e. [ X ] ( A X. A ) <-> X ( A X. A ) x ) )
3	1 2	mpan	|- ( X e. A -> ( x e. [ X ] ( A X. A ) <-> X ( A X. A ) x ) )
4		brxp	|- ( X ( A X. A ) x <-> ( X e. A /\ x e. A ) )
5	4	baib	|- ( X e. A -> ( X ( A X. A ) x <-> x e. A ) )
6	3 5	bitrd	|- ( X e. A -> ( x e. [ X ] ( A X. A ) <-> x e. A ) )
7	6	eqrdv	|- ( X e. A -> [ X ] ( A X. A ) = A )