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

Theorem bj-df-cleq 32085
Description: Candidate definition for df-cleq 2603 (the need for it is exposed in bj-ax9 32083). The similarity of the hypothesis and the conclusion 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-dfcleq 32086, which should be used instead. The proof is irrelevant since this is a proposal for an axiom.

Another definition, which would give finer control, is actually the pair of definitions where each has one implication of the present biconditional as hypothesis and conclusion. They assert that extensionality (respectively, the left-substitution axiom for the membership predicate) extends from setvars to classes. (Contributed by BJ, 24-Jun-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof of Theorem bj-df-cleq
StepHypRef Expression
1 dfcleq 2604 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 195  wal 1473   = wceq 1475  wcel 1977
This theorem was proved from axioms:  ax-ext 2590
This theorem depends on definitions:  df-cleq 2603
This theorem is referenced by:  bj-dfcleq  32086
  Copyright terms: Public domain W3C validator