Theorem bj-df-clel 32888

Description: Candidate definition for df-clel 2618 (the need for it is exposed in bj-ax8 32887). The similarity of the hypothesis and the conclusion, together with all possible dv conditions, 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-dfclel 32889, which should be used instead. The proof is irrelevant since this is a proposal for an axiom.

Note: the current definition df-clel 2618 already mentions cleljust 1998 as a justification; here, we merely propose to put it (more preciesly: its universal closure) as a hypothesis to make things more explicit. (Contributed by BJ, 27-Jun-2019.) (Proof modification is discouraged.)

Hypothesis

Ref	Expression
bj-df-clel.1	|- A. u A. v ( u e. v <-> E. w ( w = u /\ w e. v ) )

Assertion

Ref	Expression
bj-df-clel	|- ( A e. B <-> E. x ( x = A /\ x e. B ) )

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

Proof of Theorem bj-df-clel

Step	Hyp	Ref	Expression
1		df-clel 2618	1 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )

Syntax hints:   <-> wb 196   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   e. wcel 1990

This theorem depends on definitions:  df-clel 2618

This theorem is referenced by:  bj-dfclel  32889