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 | χ