Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bj-df-clel Structured version   Visualization version   GIF version

Theorem bj-df-clel 32081
Description: Candidate definition for df-clel 2606 (the need for it is exposed in bj-ax8 32080). The similarity of the hypothesis and the conclusion, together with all possible dv conditions, makes it clear that this definition merely extends to class variables something that is true for setvar variables, hence is conservative. This definition should be directly referenced only by bj-dfclel 32082, which should be used instead. The proof is irrelevant since this is a proposal for an axiom.

Note: the current definition df-clel 2606 already mentions cleljust 1985 as a justification; here, we merely propose to put it as a hypothesis to make things clearer. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
bj-df-clel.1 (𝑢𝑣 ↔ ∃𝑤(𝑤 = 𝑢𝑤𝑣))
Ref Expression
bj-df-clel (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Distinct variable groups:   𝑣,𝑢,𝑤,𝑥,𝐴   𝑢,𝐵,𝑣,𝑤,𝑥

Proof of Theorem bj-df-clel
StepHypRef Expression
1 df-clel 2606 1 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wa 383   = wceq 1475  wex 1695  wcel 1977
This theorem depends on definitions:  df-clel 2606
This theorem is referenced by:  bj-dfclel  32082
  Copyright terms: Public domain W3C validator