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

Theorem sbcg 3855
Description: Substitution for a variable not occurring in a wff does not affect it. Distinct variable form of sbcgf 3853. (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 3777 . . 3 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 dfclel 2804 . . 3 (𝐴 ∈ {𝑥𝜑} ↔ ∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}))
3 df-clab 2704 . . . . . 6 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
4 sbv 2084 . . . . . 6 ([𝑦 / 𝑥]𝜑𝜑)
53, 4bitri 274 . . . . 5 (𝑦 ∈ {𝑥𝜑} ↔ 𝜑)
65anbi2i 621 . . . 4 ((𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ (𝑦 = 𝐴𝜑))
76exbii 1843 . . 3 (∃𝑦(𝑦 = 𝐴𝑦 ∈ {𝑥𝜑}) ↔ ∃𝑦(𝑦 = 𝐴𝜑))
81, 2, 73bitrri 297 . 2 (∃𝑦(𝑦 = 𝐴𝜑) ↔ [𝐴 / 𝑥]𝜑)
9 dfclel 2804 . . . 4 (𝐴𝑉 ↔ ∃𝑦(𝑦 = 𝐴𝑦𝑉))
109biimpi 215 . . 3 (𝐴𝑉 → ∃𝑦(𝑦 = 𝐴𝑦𝑉))
11 simpr 483 . . . . . 6 ((𝑦 = 𝐴𝜑) → 𝜑)
1211ax-gen 1790 . . . . 5 𝑦((𝑦 = 𝐴𝜑) → 𝜑)
13 19.23v 1938 . . . . . 6 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) ↔ (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1413biimpi 215 . . . . 5 (∀𝑦((𝑦 = 𝐴𝜑) → 𝜑) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
1512, 14mp1i 13 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) → 𝜑))
16 2a1 28 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦𝑉 → (𝜑𝑦 = 𝐴)))
1716imp 405 . . . . . . 7 ((𝑦 = 𝐴𝑦𝑉) → (𝜑𝑦 = 𝐴))
1817ancrd 550 . . . . . 6 ((𝑦 = 𝐴𝑦𝑉) → (𝜑 → (𝑦 = 𝐴𝜑)))
1918eximi 1830 . . . . 5 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → ∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)))
20 19.37imv 1944 . . . . 5 (∃𝑦(𝜑 → (𝑦 = 𝐴𝜑)) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2119, 20syl 17 . . . 4 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (𝜑 → ∃𝑦(𝑦 = 𝐴𝜑)))
2215, 21impbid 211 . . 3 (∃𝑦(𝑦 = 𝐴𝑦𝑉) → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
2310, 22syl 17 . 2 (𝐴𝑉 → (∃𝑦(𝑦 = 𝐴𝜑) ↔ 𝜑))
248, 23bitr3id 284 1 (𝐴𝑉 → ([𝐴 / 𝑥]𝜑𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wal 1532   = wceq 1534  wex 1774  [wsb 2060  wcel 2099  {cab 2703  [wsbc 3776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-clel 2803  df-sbc 3777
This theorem is referenced by:  sbcabel  3871  csbconstg  3911  2nreu  4446  csbuni  4944  csbxp  5781  sbcfung  6583  fmptsnd  7183  csbfrecsg  8299  opsbc2ie  32404  f1od2  32635  bnj89  34566  bnj525  34583  bnj1128  34835  csbrdgg  37036  csboprabg  37037  mptsnunlem  37045  topdifinffinlem  37054  relowlpssretop  37071  rdgeqoa  37077  csbfinxpg  37095  gm-sbtru  37807  sbfal  37808  cdlemk40  40616  cdlemkid3N  40632  cdlemkid4  40633  frege70  43600  frege77  43607  frege116  43646  frege118  43648  trsbc  44216  trsbcVD  44553  csbxpgVD  44570  csbunigVD  44574
  Copyright terms: Public domain W3C validator