Theorem bj-df-cleq 32893

Description: Candidate definition for df-cleq 2615 (the need for it is exposed in bj-ax9 32890). 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 32894, 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	|- A. u A. v ( u = v <-> A. w ( w e. u <-> w e. v ) )

Assertion

Ref	Expression
bj-df-cleq	|- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Distinct variable groups:   v, u, w, x, A   u, B, v, w, x

Proof of Theorem bj-df-cleq

Step	Hyp	Ref	Expression
1		dfcleq 2616	1 |- ( A = B <-> A. x ( x e. A <-> x e. B ) )

Syntax hints:   <-> wb 196   A.wal 1481   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  bj-dfcleq  32894