Theorem sbcg 3795

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

Assertion

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

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝑉(𝑥)

Proof of Theorem sbcg

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sbc 3717	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		dfclel 2817	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}))
3		df-clab 2716	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
4		sbv 2091	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
5	3, 4	bitri 274	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
6	5	anbi2i 623	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝑦 = 𝐴 ∧ 𝜑))
7	6	exbii 1850	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))
8	1, 2, 7	3bitrri 298	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑥]𝜑)
9		dfclel 2817	. . . 4 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉))
10	9	biimpi 215	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉))
11		simpr 485	. . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝜑) → 𝜑)
12	11	ax-gen 1798	. . . . 5 ⊢ ∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑)
13		19.23v 1945	. . . . . 6 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
14	13	biimpi 215	. . . . 5 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
15	12, 14	mp1i 13	. . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
16		2a1 28	. . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 → (𝜑 → 𝑦 = 𝐴)))
17	16	imp 407	. . . . . . 7 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → 𝑦 = 𝐴))
18	17	ancrd 552	. . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → (𝑦 = 𝐴 ∧ 𝜑)))
19	18	eximi 1837	. . . . 5 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)))
20		19.37imv 1951	. . . . 5 ⊢ (∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)))
21	19, 20	syl 17	. . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)))
22	15, 21	impbid 211	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑))
23	10, 22	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑))
24	8, 23	bitr3id 285	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537   = wceq 1539  ∃wex 1782  [wsb 2067   ∈ wcel 2106  {cab 2715  [wsbc 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-clel 2816  df-sbc 3717

This theorem is referenced by:  sbcabel  3811  csbconstg  3851  2nreu  4375  csbuni  4870  csbxp  5686  sbcfung  6458  fmptsnd  7041  csbfrecsg  8100  opsbc2ie  30824  f1od2  31056  bnj89  32700  bnj525  32718  bnj1128  32970  csbrdgg  35500  csboprabg  35501  mptsnunlem  35509  topdifinffinlem  35518  relowlpssretop  35535  rdgeqoa  35541  csbfinxpg  35559  gm-sbtru  36264  sbfal  36265  cdlemk40  38931  cdlemkid3N  38947  cdlemkid4  38948  frege70  41541  frege77  41548  frege116  41587  frege118  41589  trsbc  42160  trsbcVD  42497  csbxpgVD  42514  csbunigVD  42518