Theorem wl-dfcleq.basic 38624

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

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

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

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  wl-dfcleq.just  38625  wl-dfcleq  38629