 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 33115
 Description: Candidate definition for df-clel 2720 (the need for it is exposed in bj-ax8 33114). 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 33116, which should be used instead. The proof is irrelevant since this is a proposal for an axiom. Note: the current definition df-clel 2720 already mentions cleljust 2111 as a justification; here, we merely propose to put it (more preciesly: its universal closure) as a hypothesis to make things more explicit. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)
Hypothesis
Ref Expression
bj-df-clel.1 𝑢𝑣(𝑢𝑣 ↔ ∃𝑤(𝑤 = 𝑢𝑤𝑣))
Assertion
Ref Expression
bj-df-clel (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
Distinct variable groups:   𝑣,𝑢,𝑤,𝑥,𝐴   𝑢,𝐵,𝑣,𝑤,𝑥

Proof of Theorem bj-df-clel
StepHypRef Expression
1 df-clel 2720 1 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∧ wa 383  ∀wal 1594   = wceq 1596  ∃wex 1817   ∈ wcel 2103 This theorem depends on definitions:  df-clel 2720 This theorem is referenced by:  bj-dfclel  33116
 Copyright terms: Public domain W3C validator