Theorem elcnvcnvintab

Description: Two ways of saying a set is an element of the converse of the converse of the intersection of a class. (Contributed by RP, 20-Aug-2020)

	Ref	Expression
Assertion	elcnvcnvintab	$$⊢A\in {{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \forall x\left(\phi \to A\in x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnv	$$⊢{{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}=\bigcap \left\{x|\phi \right\}\cap \left(\mathrm{V}\times \mathrm{V}\right)$$
2		incom	$$⊢\bigcap \left\{x|\phi \right\}\cap \left(\mathrm{V}\times \mathrm{V}\right)=\left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}$$
3	1 2	eqtri	$$⊢{{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}=\left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}$$
4	3	eleq2i	$$⊢A\in {{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}\leftrightarrow A\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}\right)$$
5		elinintab	$$⊢A\in \left(\left(\mathrm{V}\times \mathrm{V}\right)\cap \bigcap \left\{x|\phi \right\}\right)\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \forall x\left(\phi \to A\in x\right)\right)$$
6	4 5	bitri	$$⊢A\in {{\bigcap \left\{x|\phi \right\}}^{-1}}^{-1}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \forall x\left(\phi \to A\in x\right)\right)$$