Theorem intabssd

Description: When for each element y there is a subset A which may substituted for x such that y satisfying ch implies x satisfies ps then the intersection of all x that satisfy ps is a subclass the intersection of all y that satisfy ch . (Contributed by RP, 17-Oct-2020)

	Ref	Expression
Hypotheses	intabssd.ex	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	intabssd.sub	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜒 → 𝜓 ) )
	intabssd.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑦 )
Assertion	intabssd	⊢ ( 𝜑 → ∩ { 𝑥 ∣ 𝜓 } ⊆ ∩ { 𝑦 ∣ 𝜒 } )

Proof

Step	Hyp	Ref	Expression
1		intabssd.ex	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		intabssd.sub	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝜒 → 𝜓 ) )
3		intabssd.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝑦 )
4		eleq2	⊢ ( 𝑥 = 𝐴 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝐴 ) )
5	4	biimpd	⊢ ( 𝑥 = 𝐴 → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝐴 ) )
6	3	sseld	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐴 → 𝑧 ∈ 𝑦 ) )
7	5 6	sylan9r	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( 𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) )
8	2 7	imim12d	⊢ ( ( 𝜑 ∧ 𝑥 = 𝐴 ) → ( ( 𝜓 → 𝑧 ∈ 𝑥 ) → ( 𝜒 → 𝑧 ∈ 𝑦 ) ) )
9	1 8	spcimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝜓 → 𝑧 ∈ 𝑥 ) → ( 𝜒 → 𝑧 ∈ 𝑦 ) ) )
10	9	alrimdv	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝜓 → 𝑧 ∈ 𝑥 ) → ∀ 𝑦 ( 𝜒 → 𝑧 ∈ 𝑦 ) ) )
11		vex	⊢ 𝑧 ∈ V
12	11	elintab	⊢ ( 𝑧 ∈ ∩ { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑥 ( 𝜓 → 𝑧 ∈ 𝑥 ) )
13	11	elintab	⊢ ( 𝑧 ∈ ∩ { 𝑦 ∣ 𝜒 } ↔ ∀ 𝑦 ( 𝜒 → 𝑧 ∈ 𝑦 ) )
14	10 12 13	3imtr4g	⊢ ( 𝜑 → ( 𝑧 ∈ ∩ { 𝑥 ∣ 𝜓 } → 𝑧 ∈ ∩ { 𝑦 ∣ 𝜒 } ) )
15	14	ssrdv	⊢ ( 𝜑 → ∩ { 𝑥 ∣ 𝜓 } ⊆ ∩ { 𝑦 ∣ 𝜒 } )