Metamath Proof Explorer

Theorem cnvintabd

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

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

Proof

Step Hyp Ref Expression
1 cnvintabd.x ⊢ φ → ∃ x ψ
2 pm5.5 ⊢ ∃ x ψ → ∃ x ψ → y ∈ V × V ↔ y ∈ V × V
3 1 2 syl ⊢ φ → ∃ x ψ → y ∈ V × V ↔ y ∈ V × V
4 3 bicomd ⊢ φ → y ∈ V × V ↔ ∃ x ψ → y ∈ V × V
5 4 anbi1d ⊢ φ → y ∈ V × V ∧ ∀ x ψ → y ∈ x -1 ↔ ∃ x ψ → y ∈ V × V ∧ ∀ x ψ → y ∈ x -1
6 elcnvintab ⊢ y ∈ ⋂ x | ψ -1 ↔ y ∈ V × V ∧ ∀ x ψ → y ∈ x -1
7 vex ⊢ x ∈ V
8 7 cnvex ⊢ x -1 ∈ V
9 relcnv ⊢ Rel ⁡ x -1
10 df-rel ⊢ Rel ⁡ x -1 ↔ x -1 ⊆ V × V
11 9 10 mpbi ⊢ x -1 ⊆ V × V
12 8 11 elmapintrab ⊢ y ∈ V → y ∈ ⋂ w ∈ 𝒫 V × V | ∃ x w = x -1 ∧ ψ ↔ ∃ x ψ → y ∈ V × V ∧ ∀ x ψ → y ∈ x -1
13 12 elv ⊢ y ∈ ⋂ w ∈ 𝒫 V × V | ∃ x w = x -1 ∧ ψ ↔ ∃ x ψ → y ∈ V × V ∧ ∀ x ψ → y ∈ x -1
14 5 6 13 3bitr4g ⊢ φ → y ∈ ⋂ x | ψ -1 ↔ y ∈ ⋂ w ∈ 𝒫 V × V | ∃ x w = x -1 ∧ ψ
15 14 eqrdv ⊢ φ → ⋂ x | ψ -1 = ⋂ w ∈ 𝒫 V × V | ∃ x w = x -1 ∧ ψ