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