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

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.
StepHypRef Expression
1 df-sbc 3695 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 dfclel 2817 . . 3 (𝐴 ∈ {𝑥𝜑} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}))
3 df-clab 2715 . . . . . 6 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
4 sbv 2094 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜑)
53, 4bitri 278 . . . . 5 (𝑦 ∈ {𝑥𝜑} ↔ 𝜑)
65anbi2i 626 . . . 4 ((𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ (𝑦 = 𝐴𝜑))
76exbii 1855 . . 3 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑦(𝑦 = 𝐴𝜑))
81, 2, 73bitrri 301 . 2 (∃𝑦(𝑦 = 𝐴𝜑) ↔ [𝐴 / 𝑥]𝜑)
9 dfclel 2817 . . . 4 (𝐴𝑉 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝑉))
109biimpi 219 . . 3 (𝐴𝑉 → ∃𝑦(𝑦 = 𝐴𝑦𝑉))
11 simpr 488 . . . . . 6 ((𝑦 = 𝐴𝜑) → 𝜑)
1211ax-gen 1803 . . . . 5 𝑦((𝑦 = 𝐴𝜑) → 𝜑)
13 19.23v 1950 . . . . . 6 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1413biimpi 219 . . . . 5 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1512, 14mp1i 13 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
16 2a1 28 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑉 → (𝜑𝑦 = 𝐴)))
1716imp 410 . . . . . . 7 ((𝑦 = 𝐴𝑦𝑉) → (𝜑𝑦 = 𝐴))
1817ancrd 555 . . . . . 6 ((𝑦 = 𝐴𝑦𝑉) → (𝜑 → (𝑦 = 𝐴𝜑)))
1918eximi 1842 . . . . 5 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)))
20 19.37imv 1956 . . . . 5 (∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2119, 20syl 17 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2215, 21impbid 215 . . 3 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
2310, 22syl 17 . 2 (𝐴𝑉 → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
248, 23bitr3id 288 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator