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

Theorem sbcg 3857
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3855. (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.
StepHypRef Expression
1 df-sbc 3779 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 dfclel 2812 . . 3 (𝐴 ∈ {𝑥𝜑} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}))
3 df-clab 2711 . . . . . 6 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
4 sbv 2092 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜑)
53, 4bitri 275 . . . . 5 (𝑦 ∈ {𝑥𝜑} ↔ 𝜑)
65anbi2i 624 . . . 4 ((𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ (𝑦 = 𝐴𝜑))
76exbii 1851 . . 3 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑦(𝑦 = 𝐴𝜑))
81, 2, 73bitrri 298 . 2 (∃𝑦(𝑦 = 𝐴𝜑) ↔ [𝐴 / 𝑥]𝜑)
9 dfclel 2812 . . . 4 (𝐴𝑉 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝑉))
109biimpi 215 . . 3 (𝐴𝑉 → ∃𝑦(𝑦 = 𝐴𝑦𝑉))
11 simpr 486 . . . . . 6 ((𝑦 = 𝐴𝜑) → 𝜑)
1211ax-gen 1798 . . . . 5 𝑦((𝑦 = 𝐴𝜑) → 𝜑)
13 19.23v 1946 . . . . . 6 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1413biimpi 215 . . . . 5 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1512, 14mp1i 13 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
16 2a1 28 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑉 → (𝜑𝑦 = 𝐴)))
1716imp 408 . . . . . . 7 ((𝑦 = 𝐴𝑦𝑉) → (𝜑𝑦 = 𝐴))
1817ancrd 553 . . . . . 6 ((𝑦 = 𝐴𝑦𝑉) → (𝜑 → (𝑦 = 𝐴𝜑)))
1918eximi 1838 . . . . 5 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)))
20 19.37imv 1952 . . . . 5 (∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2119, 20syl 17 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2215, 21impbid 211 . . 3 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
2310, 22syl 17 . 2 (𝐴𝑉 → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
248, 23bitr3id 285 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540   = wceq 1542  wex 1782  [wsb 2068  wcel 2107  {cab 2710  [wsbc 3778
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 1914  ax-6 1972  ax-7 2012  ax-8 2109
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-clel 2811  df-sbc 3779
This theorem is referenced by:  sbcabel  3873  csbconstg  3913  2nreu  4442  csbuni  4941  csbxp  5776  sbcfung  6573  fmptsnd  7167  csbfrecsg  8269  opsbc2ie  31716  f1od2  31946  bnj89  33732  bnj525  33749  bnj1128  34001  csbrdgg  36210  csboprabg  36211  mptsnunlem  36219  topdifinffinlem  36228  relowlpssretop  36245  rdgeqoa  36251  csbfinxpg  36269  gm-sbtru  36974  sbfal  36975  cdlemk40  39788  cdlemkid3N  39804  cdlemkid4  39805  frege70  42684  frege77  42691  frege116  42730  frege118  42732  trsbc  43301  trsbcVD  43638  csbxpgVD  43655  csbunigVD  43659
  Copyright terms: Public domain W3C validator