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

Theorem sbc5 3786
 Description: An equivalence for class substitution. (Contributed by NM, 23-Aug-1993.) (Revised by Mario Carneiro, 12-Oct-2016.)
Assertion
Ref Expression
sbc5 ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑))
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem sbc5
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 sbcex 3768 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ V)
2 exsimpl 1870 . . 3 (∃𝑥(𝑥 = 𝐴𝜑) → ∃𝑥 𝑥 = 𝐴)
3 isset 3492 . . 3 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
42, 3sylibr 237 . 2 (∃𝑥(𝑥 = 𝐴𝜑) → 𝐴 ∈ V)
5 dfsbcq2 3761 . . 3 (𝑦 = 𝐴 → ([𝑦 / 𝑥]𝜑[𝐴 / 𝑥]𝜑))
6 eqeq2 2836 . . . . 5 (𝑦 = 𝐴 → (𝑥 = 𝑦𝑥 = 𝐴))
76anbi1d 632 . . . 4 (𝑦 = 𝐴 → ((𝑥 = 𝑦𝜑) ↔ (𝑥 = 𝐴𝜑)))
87exbidv 1923 . . 3 (𝑦 = 𝐴 → (∃𝑥(𝑥 = 𝑦𝜑) ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
9 sb5 2278 . . 3 ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦𝜑))
105, 8, 9vtoclbg 3555 . 2 (𝐴 ∈ V → ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑)))
111, 4, 10pm5.21nii 383 1 ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781  [wsb 2070   ∈ wcel 2115  Vcvv 3480  [wsbc 3758 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-12 2179  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-sbc 3759 This theorem is referenced by:  sbc6g  3787  sbc7  3789  sbciegft  3794  sbccomlem  3837  csb2  3868  rexsns  4594  sbcop1  5366  sbccom2lem  35507  pm13.192  41034  pm13.195  41037  2sbc5g  41040  iotasbc  41043  pm14.122b  41047  iotasbc5  41055  sbcpr  43964
 Copyright terms: Public domain W3C validator