Theorem wl-dfcleq.basic 38121

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

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

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

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

Syntax hints:   ↔ wb 209  ∀wal 1566   = wceq 1568   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-cleq 2753

This theorem is referenced by:  wl-dfcleq.just  38122  wl-dfcleq  38126