Theorem inintabss

Description: Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020)

	Ref	Expression
Assertion	inintabss	⊢ ( 𝐴 ∩ ∩ { 𝑥 ∣ 𝜑 } ) ⊆ ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴 ∩ 𝑥 ) ∧ 𝜑 ) }

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( 𝑢 ∈ 𝐴 → ( ∃ 𝑥 𝜑 → 𝑢 ∈ 𝐴 ) )
2	1	anim1i	⊢ ( ( 𝑢 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝜑 → 𝑢 ∈ 𝑥 ) ) → ( ( ∃ 𝑥 𝜑 → 𝑢 ∈ 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑢 ∈ 𝑥 ) ) )
3		elinintab	⊢ ( 𝑢 ∈ ( 𝐴 ∩ ∩ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝑢 ∈ 𝐴 ∧ ∀ 𝑥 ( 𝜑 → 𝑢 ∈ 𝑥 ) ) )
4		elinintrab	⊢ ( 𝑢 ∈ V → ( 𝑢 ∈ ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴 ∩ 𝑥 ) ∧ 𝜑 ) } ↔ ( ( ∃ 𝑥 𝜑 → 𝑢 ∈ 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑢 ∈ 𝑥 ) ) ) )
5	4	elv	⊢ ( 𝑢 ∈ ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴 ∩ 𝑥 ) ∧ 𝜑 ) } ↔ ( ( ∃ 𝑥 𝜑 → 𝑢 ∈ 𝐴 ) ∧ ∀ 𝑥 ( 𝜑 → 𝑢 ∈ 𝑥 ) ) )
6	2 3 5	3imtr4i	⊢ ( 𝑢 ∈ ( 𝐴 ∩ ∩ { 𝑥 ∣ 𝜑 } ) → 𝑢 ∈ ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴 ∩ 𝑥 ) ∧ 𝜑 ) } )
7	6	ssriv	⊢ ( 𝐴 ∩ ∩ { 𝑥 ∣ 𝜑 } ) ⊆ ∩ { 𝑤 ∈ 𝒫 𝐴 ∣ ∃ 𝑥 ( 𝑤 = ( 𝐴 ∩ 𝑥 ) ∧ 𝜑 ) }