Theorem wl-dfclel.basic 38018

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 36597.

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 2848).

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

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

(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 2154	. 2 ⊢ (𝑦 ∈ 𝑧 ↔ ∃𝑢(𝑢 = 𝑦 ∧ 𝑢 ∈ 𝑧))
2		cleljust 2154	. 2 ⊢ (𝑡 ∈ 𝑡 ↔ ∃𝑣(𝑣 = 𝑡 ∧ 𝑣 ∈ 𝑡))
3	1, 2	wl-df.clel 38017	1 ⊢ (𝐴 ∈ 𝐵 ↔ ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1563  ∃wex 1802   ∈ wcel 2145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-clel 2840

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