Metamath Proof Explorer

Theorem cnvcnvintabd

Description: Value of the relationship content of the intersection of a class. (Contributed by RP, 20-Aug-2020)

Ref Expression
Hypothesis cnvcnvintabd.x ⊢φ→∃xψ
Assertion cnvcnvintabd ⊢φ→⋂x|ψ-1-1=⋂w∈𝒫V×V|∃xw=x-1-1∧ψ

Proof

Step Hyp Ref Expression
1 cnvcnvintabd.x ⊢φ→∃xψ
2 cnvcnv ⊢x-1-1=x∩V×V
3 2 eleq2i ⊢y∈x-1-1↔y∈x∩V×V
4 elin ⊢y∈x∩V×V↔y∈x∧y∈V×V
5 4 rbaib ⊢y∈V×V→y∈x∩V×V↔y∈x
6 3 5 bitrid ⊢y∈V×V→y∈x-1-1↔y∈x
7 6 bicomd ⊢y∈V×V→y∈x↔y∈x-1-1
8 7 imbi2d ⊢y∈V×V→ψ→y∈x↔ψ→y∈x-1-1
9 8 albidv ⊢y∈V×V→∀xψ→y∈x↔∀xψ→y∈x-1-1
10 9 pm5.32i ⊢y∈V×V∧∀xψ→y∈x↔y∈V×V∧∀xψ→y∈x-1-1
11 pm5.5 ⊢∃xψ→∃xψ→y∈V×V↔y∈V×V
12 1 11 syl ⊢φ→∃xψ→y∈V×V↔y∈V×V
13 12 bicomd ⊢φ→y∈V×V↔∃xψ→y∈V×V
14 13 anbi1d ⊢φ→y∈V×V∧∀xψ→y∈x-1-1↔∃xψ→y∈V×V∧∀xψ→y∈x-1-1
15 10 14 bitrid ⊢φ→y∈V×V∧∀xψ→y∈x↔∃xψ→y∈V×V∧∀xψ→y∈x-1-1
16 elcnvcnvintab ⊢y∈⋂x|ψ-1-1↔y∈V×V∧∀xψ→y∈x
17 vex ⊢x∈V
18 cnvexg ⊢x∈V→x-1∈V
19 cnvexg ⊢x-1∈V→x-1-1∈V
20 17 18 19 mp2b ⊢x-1-1∈V
21 relcnv ⊢Rel⁡x-1-1
22 df-rel ⊢Rel⁡x-1-1↔x-1-1⊆V×V
23 21 22 mpbi ⊢x-1-1⊆V×V
24 20 23 elmapintrab ⊢y∈V→y∈⋂w∈𝒫V×V|∃xw=x-1-1∧ψ↔∃xψ→y∈V×V∧∀xψ→y∈x-1-1
25 24 elv ⊢y∈⋂w∈𝒫V×V|∃xw=x-1-1∧ψ↔∃xψ→y∈V×V∧∀xψ→y∈x-1-1
26 15 16 25 3bitr4g ⊢φ→y∈⋂x|ψ-1-1↔y∈⋂w∈𝒫V×V|∃xw=x-1-1∧ψ
27 26 eqrdv ⊢φ→⋂x|ψ-1-1=⋂w∈𝒫V×V|∃xw=x-1-1∧ψ