Theorem wl-dfclel.basic 37970

Description: This theorem gives a conservative extension of membership of classes, without hypotheses. Conservativity alone, however, is insufficient, since issues involving alpha-renaming can still arise, see in-ax8 36548.

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

1. Theorems whose hypotheses and conclusion contain no bound variables (see eleq1w 2844).

2. Theorems using the same bound variable throughout (see elex2 2838).

3. Theorems in which distinct bound variables arise only through implicit substitution (see eqabbw 2834).

(Contributed by BJ, 27-Jun-2019.)

Assertion

Ref	Expression
wl-dfclel.basic	⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem wl-dfclel.basic

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

Step	Hyp	Ref	Expression
1		cleljust 2150	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		cleljust 2150	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	wl-df.clel 37969	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 208   ∧ wa 399   = wceq 1559  ∃wex 1798   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-clel 2836

This theorem is referenced by:  wl-dfclel.just  37971