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 ( 𝜑 → ∃ 𝑥 𝜓 )
Assertion inintabd ( 𝜑 → ( 𝐴 { 𝑥𝜓 } ) = { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴𝑥 ) ∧ 𝜓 ) } )

Proof

Step Hyp Ref Expression
1 inintabd.x ( 𝜑 → ∃ 𝑥 𝜓 )
2 pm5.5 ( ∃ 𝑥 𝜓 → ( ( ∃ 𝑥 𝜓𝑢𝐴 ) ↔ 𝑢𝐴 ) )
3 1 2 syl ( 𝜑 → ( ( ∃ 𝑥 𝜓𝑢𝐴 ) ↔ 𝑢𝐴 ) )
4 3 bicomd ( 𝜑 → ( 𝑢𝐴 ↔ ( ∃ 𝑥 𝜓𝑢𝐴 ) ) )
5 4 anbi1d ( 𝜑 → ( ( 𝑢𝐴 ∧ ∀ 𝑥 ( 𝜓𝑢𝑥 ) ) ↔ ( ( ∃ 𝑥 𝜓𝑢𝐴 ) ∧ ∀ 𝑥 ( 𝜓𝑢𝑥 ) ) ) )
6 elinintab ( 𝑢 ∈ ( 𝐴 { 𝑥𝜓 } ) ↔ ( 𝑢𝐴 ∧ ∀ 𝑥 ( 𝜓𝑢𝑥 ) ) )
7 elinintrab ( 𝑢 ∈ V → ( 𝑢 { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴𝑥 ) ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓𝑢𝐴 ) ∧ ∀ 𝑥 ( 𝜓𝑢𝑥 ) ) ) )
8 7 elv ( 𝑢 { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴𝑥 ) ∧ 𝜓 ) } ↔ ( ( ∃ 𝑥 𝜓𝑢𝐴 ) ∧ ∀ 𝑥 ( 𝜓𝑢𝑥 ) ) )
9 5 6 8 3bitr4g ( 𝜑 → ( 𝑢 ∈ ( 𝐴 { 𝑥𝜓 } ) ↔ 𝑢 { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴𝑥 ) ∧ 𝜓 ) } ) )
10 9 eqrdv ( 𝜑 → ( 𝐴 { 𝑥𝜓 } ) = { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴𝑥 ) ∧ 𝜓 ) } )