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

Theorem cleljustab 2805
Description: Extension of cleljust 2124 from formulas of the form "setvar setvar" to formulas of the form "setvar class abstraction". This is an instance of dfclel 2897 where the containing class is a class abstraction. The same remarks as for eleq1ab 2804 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 2804 . . 3 (𝑧 = 𝑥 → (𝑧 ∈ {𝑦𝜑} ↔ 𝑥 ∈ {𝑦𝜑}))
21equsexvw 2012 . 2 (∃𝑧(𝑧 = 𝑥𝑧 ∈ {𝑦𝜑}) ↔ 𝑥 ∈ {𝑦𝜑})
32bicomi 227 1 (𝑥 ∈ {𝑦𝜑} ↔ ∃𝑧(𝑧 = 𝑥𝑧 ∈ {𝑦𝜑}))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wa 399  wex 1781  wcel 2115  {cab 2802
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
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator