MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbcg Structured version   Visualization version   GIF version

Theorem sbcg 3863
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3861. (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.
StepHypRef Expression
1 df-sbc 3789 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 dfclel 2817 . . 3 (𝐴 ∈ {𝑥𝜑} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}))
3 df-clab 2715 . . . . . 6 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
4 sbv 2088 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜑)
53, 4bitri 275 . . . . 5 (𝑦 ∈ {𝑥𝜑} ↔ 𝜑)
65anbi2i 623 . . . 4 ((𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ (𝑦 = 𝐴𝜑))
76exbii 1848 . . 3 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑦(𝑦 = 𝐴𝜑))
81, 2, 73bitrri 298 . 2 (∃𝑦(𝑦 = 𝐴𝜑) ↔ [𝐴 / 𝑥]𝜑)
9 dfclel 2817 . . . 4 (𝐴𝑉 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝑉))
109biimpi 216 . . 3 (𝐴𝑉 → ∃𝑦(𝑦 = 𝐴𝑦𝑉))
11 simpr 484 . . . . . 6 ((𝑦 = 𝐴𝜑) → 𝜑)
1211ax-gen 1795 . . . . 5 𝑦((𝑦 = 𝐴𝜑) → 𝜑)
13 19.23v 1942 . . . . . 6 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1413biimpi 216 . . . . 5 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1512, 14mp1i 13 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
16 2a1 28 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑉 → (𝜑𝑦 = 𝐴)))
1716imp 406 . . . . . . 7 ((𝑦 = 𝐴𝑦𝑉) → (𝜑𝑦 = 𝐴))
1817ancrd 551 . . . . . 6 ((𝑦 = 𝐴𝑦𝑉) → (𝜑 → (𝑦 = 𝐴𝜑)))
1918eximi 1835 . . . . 5 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)))
20 19.37imv 1947 . . . . 5 (∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2119, 20syl 17 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2215, 21impbid 212 . . 3 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
2310, 22syl 17 . 2 (𝐴𝑉 → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
248, 23bitr3id 285 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538   = wceq 1540  wex 1779  [wsb 2064  wcel 2108  {cab 2714  [wsbc 3788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-clel 2816  df-sbc 3789
This theorem is referenced by:  sbcabel  3878  csbconstg  3918  2nreu  4444  csbuni  4936  csbxp  5785  sbcfung  6590  fmptsnd  7189  csbfrecsg  8309  opsbc2ie  32495  f1od2  32732  bnj89  34735  bnj525  34752  bnj1128  35004  csbrdgg  37330  csboprabg  37331  mptsnunlem  37339  topdifinffinlem  37348  relowlpssretop  37365  rdgeqoa  37371  csbfinxpg  37389  gm-sbtru  38113  sbfal  38114  cdlemk40  40919  cdlemkid3N  40935  cdlemkid4  40936  frege70  43946  frege77  43953  frege116  43992  frege118  43994  trsbc  44560  trsbcVD  44897  csbxpgVD  44914  csbunigVD  44918
  Copyright terms: Public domain W3C validator