Metamath Proof Explorer

Theorem inintabd

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

Ref Expression
Hypothesis inintabd.x ⊢ φ → ∃ x ψ
Assertion inintabd ⊢ φ → A ∩ ⋂ x | ψ = ⋂ w ∈ 𝒫 A | ∃ x w = A ∩ x ∧ ψ

Proof

Step Hyp Ref Expression
1 inintabd.x ⊢ φ → ∃ x ψ
2 pm5.5 ⊢ ∃ x ψ → ∃ x ψ → u ∈ A ↔ u ∈ A
3 1 2 syl ⊢ φ → ∃ x ψ → u ∈ A ↔ u ∈ A
4 3 bicomd ⊢ φ → u ∈ A ↔ ∃ x ψ → u ∈ A
5 4 anbi1d ⊢ φ → u ∈ A ∧ ∀ x ψ → u ∈ x ↔ ∃ x ψ → u ∈ A ∧ ∀ x ψ → u ∈ x
6 elinintab ⊢ u ∈ A ∩ ⋂ x | ψ ↔ u ∈ A ∧ ∀ x ψ → u ∈ x
7 elinintrab ⊢ u ∈ V → u ∈ ⋂ w ∈ 𝒫 A | ∃ x w = A ∩ x ∧ ψ ↔ ∃ x ψ → u ∈ A ∧ ∀ x ψ → u ∈ x
8 7 elv ⊢ u ∈ ⋂ w ∈ 𝒫 A | ∃ x w = A ∩ x ∧ ψ ↔ ∃ x ψ → u ∈ A ∧ ∀ x ψ → u ∈ x
9 5 6 8 3bitr4g ⊢ φ → u ∈ A ∩ ⋂ x | ψ ↔ u ∈ ⋂ w ∈ 𝒫 A | ∃ x w = A ∩ x ∧ ψ
10 9 eqrdv ⊢ φ → A ∩ ⋂ x | ψ = ⋂ w ∈ 𝒫 A | ∃ x w = A ∩ x ∧ ψ