Theorem wl-dfcleq.basic 38508

Description: This theorem is a conservative extension of ax-ext 2732 to classes, with no hypotheses. It is not complete, since ax-8 2146 can be derived (see in-ax8 37088) 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 2757).

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

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

Remark: the proof uses axextb 2735 to prove the hypothesis of df-cleq 2752 that is a degenerate instance, but it could be proved also from minimal propositional calculus and { ax-gen 1827, equid 2044 }. (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 2735	. 2 ⊢ (𝑦 = 𝑧 ↔ ∀𝑢(𝑢 ∈ 𝑦 ↔ 𝑢 ∈ 𝑧))
2		axextb 2735	. 2 ⊢ (𝑡 = 𝑡 ↔ ∀𝑣(𝑣 ∈ 𝑡 ↔ 𝑣 ∈ 𝑡))
3	1, 2	wl-df.cleq 38507	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  wl-dfcleq.just  38509  wl-dfcleq  38513