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

Theorem cleljustab 2716
Description: Extension of cleljust 2114 from formulas of the form "setvar setvar" to formulas of the form "setvar class abstraction". This is an instance of dfclel 2815 where the containing class is a class abstraction. The same remarks as for eleq1ab 2715 apply. (Contributed by BJ, 8-Nov-2021.) (Proof shortened by Steven Nguyen, 19-May-2023.)
Assertion
Ref Expression
cleljustab (𝑥 ∈ {𝑦𝜑} ↔ ∃𝑧(𝑧 = 𝑥𝑧 ∈ {𝑦𝜑}))
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝜑,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem cleljustab
StepHypRef Expression
1 eleq1ab 2715 . . 3 (𝑧 = 𝑥 → (𝑧 ∈ {𝑦𝜑} ↔ 𝑥 ∈ {𝑦𝜑}))
21equsexvw 2007 . 2 (∃𝑧(𝑧 = 𝑥𝑧 ∈ {𝑦𝜑}) ↔ 𝑥 ∈ {𝑦𝜑})
32bicomi 223 1 (𝑥 ∈ {𝑦𝜑} ↔ ∃𝑧(𝑧 = 𝑥𝑧 ∈ {𝑦𝜑}))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396  wex 1780  wcel 2105  {cab 2713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator