# Metamath Proof Explorer

## 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}↔\left({A}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\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}×\mathrm{V}\right)$
2 incom ${⊢}\bigcap \left\{{x}|{\phi }\right\}\cap \left(\mathrm{V}×\mathrm{V}\right)=\left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}$
3 1 2 eqtri ${⊢}{{\bigcap \left\{{x}|{\phi }\right\}}^{-1}}^{-1}=\left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}$
4 3 eleq2i ${⊢}{A}\in {{\bigcap \left\{{x}|{\phi }\right\}}^{-1}}^{-1}↔{A}\in \left(\left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}\right)$
5 elinintab ${⊢}{A}\in \left(\left(\mathrm{V}×\mathrm{V}\right)\cap \bigcap \left\{{x}|{\phi }\right\}\right)↔\left({A}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {A}\in {x}\right)\right)$
6 4 5 bitri ${⊢}{A}\in {{\bigcap \left\{{x}|{\phi }\right\}}^{-1}}^{-1}↔\left({A}\in \left(\mathrm{V}×\mathrm{V}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {A}\in {x}\right)\right)$