Theorem sbcg

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf . (Contributed by Alan Sare, 10-Nov-2012) Reduce axiom usage. (Revised by Gino Giotto, 12-Oct-2024)

	Ref	Expression
Assertion	sbcg	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		df-sbc	$$⊢\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow A\in \left\{x|\phi \right\}$$
2		dfclel	$$⊢A\in \left\{x|\phi \right\}\leftrightarrow \exists y\left(y=A\wedge y\in \left\{x|\phi \right\}\right)$$
3		df-clab	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \left[y/x\right]\phi$$
4		sbv	$$⊢\left[y/x\right]\phi \leftrightarrow \phi$$
5	3 4	bitri	$$⊢y\in \left\{x|\phi \right\}\leftrightarrow \phi$$
6	5	anbi2i	$$⊢\left(y=A\wedge y\in \left\{x|\phi \right\}\right)\leftrightarrow \left(y=A\wedge \phi \right)$$
7	6	exbii	$$⊢\exists y\left(y=A\wedge y\in \left\{x|\phi \right\}\right)\leftrightarrow \exists y\left(y=A\wedge \phi \right)$$
8	1 2 7	3bitrri	$$⊢\exists y\left(y=A\wedge \phi \right)\leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
9		dfclel	$$⊢A\in V\leftrightarrow \exists y\left(y=A\wedge y\in V\right)$$
10	9	biimpi	$$⊢A\in V\to \exists y\left(y=A\wedge y\in V\right)$$
11		simpr	$$⊢\left(y=A\wedge \phi \right)\to \phi$$
12	11	ax-gen	$$⊢\forall y\left(\left(y=A\wedge \phi \right)\to \phi \right)$$
13		19.23v	$$⊢\forall y\left(\left(y=A\wedge \phi \right)\to \phi \right)\leftrightarrow \left(\exists y\left(y=A\wedge \phi \right)\to \phi \right)$$
14	13	biimpi	$$⊢\forall y\left(\left(y=A\wedge \phi \right)\to \phi \right)\to \left(\exists y\left(y=A\wedge \phi \right)\to \phi \right)$$
15	12 14	mp1i	$$⊢\exists y\left(y=A\wedge y\in V\right)\to \left(\exists y\left(y=A\wedge \phi \right)\to \phi \right)$$
16		2a1	$$⊢y=A\to \left(y\in V\to \left(\phi \to y=A\right)\right)$$
17	16	imp	$$⊢\left(y=A\wedge y\in V\right)\to \left(\phi \to y=A\right)$$
18	17	ancrd	$$⊢\left(y=A\wedge y\in V\right)\to \left(\phi \to \left(y=A\wedge \phi \right)\right)$$
19	18	eximi	$$⊢\exists y\left(y=A\wedge y\in V\right)\to \exists y\left(\phi \to \left(y=A\wedge \phi \right)\right)$$
20		19.37imv	$$⊢\exists y\left(\phi \to \left(y=A\wedge \phi \right)\right)\to \left(\phi \to \exists y\left(y=A\wedge \phi \right)\right)$$
21	19 20	syl	$$⊢\exists y\left(y=A\wedge y\in V\right)\to \left(\phi \to \exists y\left(y=A\wedge \phi \right)\right)$$
22	15 21	impbid	$$⊢\exists y\left(y=A\wedge y\in V\right)\to \left(\exists y\left(y=A\wedge \phi \right)\leftrightarrow \phi \right)$$
23	10 22	syl	$$⊢A\in V\to \left(\exists y\left(y=A\wedge \phi \right)\leftrightarrow \phi \right)$$
24	8 23	bitr3id	$$⊢A\in V\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$