Theorem sbcimdv

Description: Substitution analogue of Theorem 19.20 of Margaris p. 90 ( alim ). (Contributed by NM, 11-Nov-2005) (Revised by NM, 17-Aug-2018) (Proof shortened by JJ, 7-Jul-2021) Reduce axiom usage. (Revised by GG, 12-Oct-2024)

	Ref	Expression
Hypothesis	sbcimdv.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
Assertion	sbcimdv	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbcimdv.1	$$⊢\phi \to \left(\psi \to \chi \right)$$
2		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow A\in \left\{x|\psi \right\}$$
3		dfclel	$$⊢A\in \left\{x|\psi \right\}\leftrightarrow \exists y\left(y=A\wedge y\in \left\{x|\psi \right\}\right)$$
4		df-clab	$$⊢y\in \left\{x|\psi \right\}\leftrightarrow \left[y/x\right]\psi$$
5	4	anbi2i	$$⊢\left(y=A\wedge y\in \left\{x|\psi \right\}\right)\leftrightarrow \left(y=A\wedge \left[y/x\right]\psi \right)$$
6	5	exbii	$$⊢\exists y\left(y=A\wedge y\in \left\{x|\psi \right\}\right)\leftrightarrow \exists y\left(y=A\wedge \left[y/x\right]\psi \right)$$
7	2 3 6	3bitri	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \leftrightarrow \exists y\left(y=A\wedge \left[y/x\right]\psi \right)$$
8	7	biimpi	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \to \exists y\left(y=A\wedge \left[y/x\right]\psi \right)$$
9	1	sbimdv	$$⊢\phi \to \left(\left[y/x\right]\psi \to \left[y/x\right]\chi \right)$$
10	9	anim2d	$$⊢\phi \to \left(\left(y=A\wedge \left[y/x\right]\psi \right)\to \left(y=A\wedge \left[y/x\right]\chi \right)\right)$$
11	10	eximdv	$$⊢\phi \to \left(\exists y\left(y=A\wedge \left[y/x\right]\psi \right)\to \exists y\left(y=A\wedge \left[y/x\right]\chi \right)\right)$$
12		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \leftrightarrow A\in \left\{x|\chi \right\}$$
13		dfclel	$$⊢A\in \left\{x|\chi \right\}\leftrightarrow \exists y\left(y=A\wedge y\in \left\{x|\chi \right\}\right)$$
14		df-clab	$$⊢y\in \left\{x|\chi \right\}\leftrightarrow \left[y/x\right]\chi$$
15	14	anbi2i	$$⊢\left(y=A\wedge y\in \left\{x|\chi \right\}\right)\leftrightarrow \left(y=A\wedge \left[y/x\right]\chi \right)$$
16	15	exbii	$$⊢\exists y\left(y=A\wedge y\in \left\{x|\chi \right\}\right)\leftrightarrow \exists y\left(y=A\wedge \left[y/x\right]\chi \right)$$
17	12 13 16	3bitrri	$$⊢\exists y\left(y=A\wedge \left[y/x\right]\chi \right)\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi$$
18	17	biimpi	$$⊢\exists y\left(y=A\wedge \left[y/x\right]\chi \right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi$$
19	8 11 18	syl56	$$⊢\phi \to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\psi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\chi \right)$$