Metamath Proof Explorer

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 ⊢ φ → A ∈ V
intabssd.sub ⊢ φ ∧ x = A → χ → ψ
intabssd.ss ⊢ φ → A ⊆ y
Assertion intabssd ⊢ φ → ⋂ x | ψ ⊆ ⋂ y | χ

Proof

Step Hyp Ref Expression
1 intabssd.ex ⊢ φ → A ∈ V
2 intabssd.sub ⊢ φ ∧ x = A → χ → ψ
3 intabssd.ss ⊢ φ → A ⊆ y
4 eleq2 ⊢ x = A → z ∈ x ↔ z ∈ A
5 4 biimpd ⊢ x = A → z ∈ x → z ∈ A
6 3 sseld ⊢ φ → z ∈ A → z ∈ y
7 5 6 sylan9r ⊢ φ ∧ x = A → z ∈ x → z ∈ y
8 2 7 imim12d ⊢ φ ∧ x = A → ψ → z ∈ x → χ → z ∈ y
9 1 8 spcimdv ⊢ φ → ∀ x ψ → z ∈ x → χ → z ∈ y
10 9 alrimdv ⊢ φ → ∀ x ψ → z ∈ x → ∀ y χ → z ∈ y
11 vex ⊢ z ∈ V
12 11 elintab ⊢ z ∈ ⋂ x | ψ ↔ ∀ x ψ → z ∈ x
13 11 elintab ⊢ z ∈ ⋂ y | χ ↔ ∀ y χ → z ∈ y
14 10 12 13 3imtr4g ⊢ φ → z ∈ ⋂ x | ψ → z ∈ ⋂ y | χ
15 14 ssrdv ⊢ φ → ⋂ x | ψ ⊆ ⋂ y | χ