Theorem elcnvintab

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

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left(y\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)=\left(y\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)$$
2	1	elcnvlem	$$⊢A\in {\bigcap \left\{x|\phi \right\}}^{-1}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(y\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)\left(A\right)\in \bigcap \left\{x|\phi \right\}\right)$$
3	1	elcnvlem	$$⊢A\in x^{-1}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \left(y\in \left(\mathrm{V}\times \mathrm{V}\right)⟼⟨2^{nd}\left(y\right),1^{st}\left(y\right)⟩\right)\left(A\right)\in x\right)$$
4	2 3	elmapintab	$$⊢A\in {\bigcap \left\{x|\phi \right\}}^{-1}\leftrightarrow \left(A\in \left(\mathrm{V}\times \mathrm{V}\right)\wedge \forall x\left(\phi \to A\in x^{-1}\right)\right)$$