dfcoels

Description: Alternate definition of the class of coelements on the class A . (Contributed by Peter Mazsa, 20-Apr-2019)

		Ref	Expression
	Assertion	dfcoels	$⊢ \sim A = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$

Step	Hyp	Ref	Expression
1		df-coels	$⊢ \sim A = ≀ ({E^{-1} ↾}_{A})$
2		1cossres	$⊢ ≀ ({E^{-1} ↾}_{A}) = \{⟨x, y⟩ \| \exists u \in A (u E^{-1} x \land u E^{-1} y)\}$
3		brcnvep	$⊢ u \in V \to (u E^{-1} x \leftrightarrow x \in u)$
4	3	elv	$⊢ u E^{-1} x \leftrightarrow x \in u$
5		brcnvep	$⊢ u \in V \to (u E^{-1} y \leftrightarrow y \in u)$
6	5	elv	$⊢ u E^{-1} y \leftrightarrow y \in u$
7	4 6	anbi12i	$⊢ (u E^{-1} x \land u E^{-1} y) \leftrightarrow (x \in u \land y \in u)$
8	7	rexbii	$⊢ \exists u \in A (u E^{-1} x \land u E^{-1} y) \leftrightarrow \exists u \in A (x \in u \land y \in u)$
9	8	opabbii	$⊢ \{⟨x, y⟩ \| \exists u \in A (u E^{-1} x \land u E^{-1} y)\} = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$
10	1 2 9	3eqtri	$⊢ \sim A = \{⟨x, y⟩ \| \exists u \in A (x \in u \land y \in u)\}$

Metamath Proof Explorer