Theorem sbcg 3774

Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3772. (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 3695	. . 3 ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝐴 ∈ {𝑥 ∣ 𝜑})
2		dfclel 2817	. . 3 ⊢ (𝐴 ∈ {𝑥 ∣ 𝜑} ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}))
3		df-clab 2715	. . . . . 6 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
4		sbv 2094	. . . . . 6 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜑)
5	3, 4	bitri 278	. . . . 5 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝜑)
6	5	anbi2i 626	. . . 4 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ (𝑦 = 𝐴 ∧ 𝜑))
7	6	exbii 1855	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ {𝑥 ∣ 𝜑}) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝜑))
8	1, 2, 7	3bitrri 301	. 2 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ [𝐴 / 𝑥]𝜑)
9		dfclel 2817	. . . 4 ⊢ (𝐴 ∈ 𝑉 ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉))
10	9	biimpi 219	. . 3 ⊢ (𝐴 ∈ 𝑉 → ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉))
11		simpr 488	. . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝜑) → 𝜑)
12	11	ax-gen 1803	. . . . 5 ⊢ ∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑)
13		19.23v 1950	. . . . . 6 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
14	13	biimpi 219	. . . . 5 ⊢ (∀𝑦((𝑦 = 𝐴 ∧ 𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
15	12, 14	mp1i 13	. . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) → 𝜑))
16		2a1 28	. . . . . . . 8 ⊢ (𝑦 = 𝐴 → (𝑦 ∈ 𝑉 → (𝜑 → 𝑦 = 𝐴)))
17	16	imp 410	. . . . . . 7 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → 𝑦 = 𝐴))
18	17	ancrd 555	. . . . . 6 ⊢ ((𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → (𝑦 = 𝐴 ∧ 𝜑)))
19	18	eximi 1842	. . . . 5 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)))
20		19.37imv 1956	. . . . 5 ⊢ (∃𝑦(𝜑 → (𝑦 = 𝐴 ∧ 𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)))
21	19, 20	syl 17	. . . 4 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴 ∧ 𝜑)))
22	15, 21	impbid 215	. . 3 ⊢ (∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝑉) → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑))
23	10, 22	syl 17	. 2 ⊢ (𝐴 ∈ 𝑉 → (∃𝑦(𝑦 = 𝐴 ∧ 𝜑) ↔ 𝜑))
24	8, 23	bitr3id 288	1 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]𝜑 ↔ 𝜑))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1541   = wceq 1543  ∃wex 1787  [wsb 2070   ∈ wcel 2110  {cab 2714  [wsbc 3694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2071  df-clab 2715  df-clel 2816  df-sbc 3695

This theorem is referenced by:  sbcabel  3790  csbconstg  3830  2nreu  4356  csbuni  4850  csbxp  5647  sbcfung  6404  fmptsnd  6984  opsbc2ie  30543  f1od2  30776  bnj89  32412  bnj525  32430  bnj1128  32683  csbwrecsg  35235  csbrdgg  35237  csboprabg  35238  mptsnunlem  35246  topdifinffinlem  35255  relowlpssretop  35272  rdgeqoa  35278  csbfinxpg  35296  gm-sbtru  36001  sbfal  36002  cdlemk40  38668  cdlemkid3N  38684  cdlemkid4  38685  frege70  41218  frege77  41225  frege116  41264  frege118  41266  trsbc  41833  trsbcVD  42170  csbxpgVD  42187  csbunigVD  42191