Theorem sbcg 3870

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3868. (Contributed by Alan Sare, 10-Nov-2012.) Reduce axiom usage. (Revised by GG, 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 3792	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		dfclel 2815	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}))
3		df-clab 2713	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
4		sbv 2086	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
5	3, 4	bitri 275	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
6	5	anbi2i 623	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝑦 = 𝐴 ∧ 𝜑))
7	6	exbii 1845	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))
8	1, 2, 7	3bitrri 298	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑥]𝜑)
9		dfclel 2815	. . . 4 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉))
10	9	biimpi 216	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉))
11		simpr 484	. . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝜑) → 𝜑)
12	11	ax-gen 1792	. . . . 5 ⊢ ∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑)
13		19.23v 1940	. . . . . 6 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
14	13	biimpi 216	. . . . 5 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
15	12, 14	mp1i 13	. . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
16		2a1 28	. . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 → (𝜑 → 𝑦 = 𝐴)))
17	16	imp 406	. . . . . . 7 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → 𝑦 = 𝐴))
18	17	ancrd 551	. . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → (𝑦 = 𝐴 ∧ 𝜑)))
19	18	eximi 1832	. . . . 5 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)))
20		19.37imv 1945	. . . . 5 ⊢ (∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)))
21	19, 20	syl 17	. . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)))
22	15, 21	impbid 212	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑))
23	10, 22	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑))
24	8, 23	bitr3id 285	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1535   = wceq 1537  ∃wex 1776  [wsb 2062   ∈ wcel 2106  {cab 2712  [wsbc 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-clel 2814  df-sbc 3792

This theorem is referenced by:  sbcabel  3887  csbconstg  3927  2nreu  4450  csbuni  4941  csbxp  5788  sbcfung  6592  fmptsnd  7189  csbfrecsg  8308  opsbc2ie  32504  f1od2  32739  bnj89  34714  bnj525  34731  bnj1128  34983  csbrdgg  37312  csboprabg  37313  mptsnunlem  37321  topdifinffinlem  37330  relowlpssretop  37347  rdgeqoa  37353  csbfinxpg  37371  gm-sbtru  38093  sbfal  38094  cdlemk40  40900  cdlemkid3N  40916  cdlemkid4  40917  frege70  43923  frege77  43930  frege116  43969  frege118  43971  trsbc  44538  trsbcVD  44875  csbxpgVD  44892  csbunigVD  44896