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

Step	Hyp	Ref	Expression
1		dfcleq 2765	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

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