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

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

Proof of Theorem sbc5
StepHypRef Expression
1 df-sbc 3792 . 2 ([𝐴 / 𝑥]𝜑𝐴 ∈ {𝑥𝜑})
2 clelab 2885 . 2 (𝐴 ∈ {𝑥𝜑} ↔ ∃𝑥(𝑥 = 𝐴𝜑))
31, 2bitri 275 1 ([𝐴 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝐴𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  wex 1776  wcel 2106  {cab 2712  [wsbc 3791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792
This theorem is referenced by:  sbc6gOLD  3822  sbc7  3824  sbciegftOLD  3830  sbccomlemOLD  3879  csb2  3910  rexsns  4676  sbcop1  5499  sbccom2lem  38111  pm13.192  44406  pm13.195  44409  2sbc5g  44412  iotasbc  44415  pm14.122b  44419  iotasbc5  44427  sbcpr  47446
  Copyright terms: Public domain W3C validator