Theorem wl-dfcleq.basic 38265

Description: This theorem is a conservative extension of ax-ext 2734 to classes, with no hypotheses. It is not complete, since ax-8 2147 can be derived (see in-ax8 36846) 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 1828, equid 2045 }. (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 38264	1 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754

This theorem is used by:  wl-dfcleq.just  38266  wl-dfcleq  38270