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

Theorem cleljustab 2710
Description: Extension of cleljust 2113 from formulas of the form "setvar setvar" to formulas of the form "setvar class abstraction". This is an instance of dfclel 2809 where the containing class is a class abstraction. The same remarks as for eleq1ab 2709 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 2709 . . 3 (𝑧 = 𝑥 → (𝑧 ∈ {𝑦𝜑} ↔ 𝑥 ∈ {𝑦𝜑}))
21equsexvw 2006 . 2 (∃𝑧(𝑧 = 𝑥𝑧 ∈ {𝑦𝜑}) ↔ 𝑥 ∈ {𝑦𝜑})
32bicomi 223 1 (𝑥 ∈ {𝑦𝜑} ↔ ∃𝑧(𝑧 = 𝑥𝑧 ∈ {𝑦𝜑}))
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 394  wex 1779  wcel 2104  {cab 2707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator