Theorem wl-dfcleq.basic 38183

Description: This theorem is a conservative extension of ax-ext 2734 to classes, with no hypotheses. It is not complete, since ax-8 2144 can be derived (see in-ax8 36764) via alpha-renaming.

Although unsuitable for general use, it is adequate for the development of theorems unaffected by alpha-renaming, including:

1. Theorems with no bound variables in the hypotheses or conclusion (see eqriv 2759).

2. Theorems using the same bound variable throughout (see abbib 2831).

3. Theorems with distinct bound variables arising only through implicit substitution (see eqabbw 2835).

Remark: the proof uses axextb 2737 to prove the hypothesis of df-cleq 2754 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1824, equid 2041 }. (Contributed by NM, 15-Sep-1993.) (Revised by BJ, 24-Jun-2019.)

Assertion

Ref	Expression
wl-dfcleq.basic	⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-dfcleq.basic

Dummy variables 𝑦 𝑧 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axextb 2737	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2737	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	wl-df.cleq 38182	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1567   = wceq 1569   ∈ wcel 2142

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754

This theorem is used by:  wl-dfcleq.just  38184  wl-dfcleq  38188