 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.)
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 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