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 | ∃ x w = 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 | ∃ x w = x -1 -1 ∧ ψ ↔ ∃ x ψ → y ∈ V × V ∧ ∀ x ψ → y ∈ x -1 -1
25 24 elv ⊢ y ∈ ⋂ w ∈ 𝒫 V × V | ∃ x w = 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 | ∃ x w = x -1 -1 ∧ ψ
27 26 eqrdv ⊢ φ → ⋂ x | ψ -1 -1 = ⋂ w ∈ 𝒫 V × V | ∃ x w = x -1 -1 ∧ ψ