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

Theorem sbcg 3856
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3854. (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 3778 . . 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 3777
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 3778
This theorem is referenced by:  sbcabel  3872  csbconstg  3912  2nreu  4441  csbuni  4940  csbxp  5774  sbcfung  6570  fmptsnd  7164  csbfrecsg  8266  opsbc2ie  31704  f1od2  31934  bnj89  33721  bnj525  33738  bnj1128  33990  csbrdgg  36199  csboprabg  36200  mptsnunlem  36208  topdifinffinlem  36217  relowlpssretop  36234  rdgeqoa  36240  csbfinxpg  36258  gm-sbtru  36963  sbfal  36964  cdlemk40  39777  cdlemkid3N  39793  cdlemkid4  39794  frege70  42670  frege77  42677  frege116  42716  frege118  42718  trsbc  43287  trsbcVD  43624  csbxpgVD  43641  csbunigVD  43645
  Copyright terms: Public domain W3C validator