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 33222
Description: Candidate definition for df-cleq 2764 (the need for it is exposed in bj-ax9 33219). 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 33223, 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.)

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

Proof of Theorem bj-df-cleq
StepHypRef Expression
1 dfcleq 2765 1 (𝐴 = 𝐵 ↔ ∀𝑥(𝑥𝐴𝑥𝐵))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1629   = wceq 1631  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764
This theorem is referenced by:  bj-dfcleq  33223
  Copyright terms: Public domain W3C validator