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 GG, 12-Oct-2024)

	Ref	Expression
Assertion	sbcg	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-sbc	⊢ ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝐴 ∈ { 𝑥 ∣ 𝜑 } )
2		dfclel	⊢ ( 𝐴 ∈ { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
3		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
4		sbv	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 )
5	3 4	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
6	5	anbi2i	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝑦 = 𝐴 ∧ 𝜑 ) )
7	6	exbii	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) )
8	1 2 7	3bitrri	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ↔ [ 𝐴 / 𝑥 ] 𝜑 )
9		dfclel	⊢ ( 𝐴 ∈ 𝑉 ↔ ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) )
10	9	biimpi	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) )
11		simpr	⊢ ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 )
12	11	ax-gen	⊢ ∀ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 )
13		19.23v	⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) ↔ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) )
14	13	biimpi	⊢ ( ∀ 𝑦 ( ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) )
15	12 14	mp1i	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) → 𝜑 ) )
16		2a1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ 𝑉 → ( 𝜑 → 𝑦 = 𝐴 ) ) )
17	16	imp	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( 𝜑 → 𝑦 = 𝐴 ) )
18	17	ancrd	⊢ ( ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( 𝜑 → ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
19	18	eximi	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ∃ 𝑦 ( 𝜑 → ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
20		19.37imv	⊢ ( ∃ 𝑦 ( 𝜑 → ( 𝑦 = 𝐴 ∧ 𝜑 ) ) → ( 𝜑 → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
21	19 20	syl	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( 𝜑 → ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ) )
22	15 21	impbid	⊢ ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉 ) → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ↔ 𝜑 ) )
23	10 22	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ∃ 𝑦 ( 𝑦 = 𝐴 ∧ 𝜑 ) ↔ 𝜑 ) )
24	8 23	bitr3id	⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 / 𝑥 ] 𝜑 ↔ 𝜑 ) )