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	$$⊢\phi \to A\in V$$
	intabssd.sub	$$⊢\left(\phi \wedge x=A\right)\to \left(\chi \to \psi \right)$$
	intabssd.ss	$$⊢\phi \to A\subseteq y$$
Assertion	intabssd	$$⊢\phi \to \bigcap \left\{x|\psi \right\}\subseteq \bigcap \left\{y|\chi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		intabssd.ex	$$⊢\phi \to A\in V$$
2		intabssd.sub	$$⊢\left(\phi \wedge x=A\right)\to \left(\chi \to \psi \right)$$
3		intabssd.ss	$$⊢\phi \to A\subseteq y$$
4		eleq2	$$⊢x=A\to \left(z\in x\leftrightarrow z\in A\right)$$
5	4	biimpd	$$⊢x=A\to \left(z\in x\to z\in A\right)$$
6	3	sseld	$$⊢\phi \to \left(z\in A\to z\in y\right)$$
7	5 6	sylan9r	$$⊢\left(\phi \wedge x=A\right)\to \left(z\in x\to z\in y\right)$$
8	2 7	imim12d	$$⊢\left(\phi \wedge x=A\right)\to \left(\left(\psi \to z\in x\right)\to \left(\chi \to z\in y\right)\right)$$
9	1 8	spcimdv	$$⊢\phi \to \left(\forall x\left(\psi \to z\in x\right)\to \left(\chi \to z\in y\right)\right)$$
10	9	alrimdv	$$⊢\phi \to \left(\forall x\left(\psi \to z\in x\right)\to \forall y\left(\chi \to z\in y\right)\right)$$
11		vex	$$⊢z\in \mathrm{V}$$
12	11	elintab	$$⊢z\in \bigcap \left\{x|\psi \right\}\leftrightarrow \forall x\left(\psi \to z\in x\right)$$
13	11	elintab	$$⊢z\in \bigcap \left\{y|\chi \right\}\leftrightarrow \forall y\left(\chi \to z\in y\right)$$
14	10 12 13	3imtr4g	$$⊢\phi \to \left(z\in \bigcap \left\{x|\psi \right\}\to z\in \bigcap \left\{y|\chi \right\}\right)$$
15	14	ssrdv	$$⊢\phi \to \bigcap \left\{x|\psi \right\}\subseteq \bigcap \left\{y|\chi \right\}$$