Theorem abeq2 2143

Description: Equality of a class variable and a class abstraction (also called a class builder). Theorem 5.1 of [Quine] p. 34. This theorem shows the relationship between expressions with class abstractions and expressions with class variables. Note that abbi 2148 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting a class abstraction for each class variable.

Class variables can always be eliminated from a theorem to result in an equivalent theorem with wff variables, and vice-versa. The idea is roughly as follows. To convert a theorem with a wff variable φ (that has a free variable x) to a theorem with a class variable A, we substitute x ∈ A for φ throughout and simplify, where A is a new class variable not already in the wff. Conversely, to convert a theorem with a class variable A to one with φ, we substitute {x ∣ φ} for A throughout and simplify, where x and φ are new set and wff variables not already in the wff. For more information on class variables, see Quine pp. 15-21 and/or Takeuti and Zaring pp. 10-13. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
abeq2	⊢ (A = {x ∣ φ} ↔ ∀x(x ∈ A ↔ φ))

Distinct variable group:   x,A

Allowed substitution hint:   φ(x)

Proof of Theorem abeq2

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-17 1416	. . 3 ⊢ (y ∈ A → ∀x y ∈ A)
2		hbab1 2026	. . 3 ⊢ (y ∈ {x ∣ φ} → ∀x y ∈ {x ∣ φ})
3	1, 2	cleqh 2134	. 2 ⊢ (A = {x ∣ φ} ↔ ∀x(x ∈ A ↔ x ∈ {x ∣ φ}))
4		abid 2025	. . . 4 ⊢ (x ∈ {x ∣ φ} ↔ φ)
5	4	bibi2i 216	. . 3 ⊢ ((x ∈ A ↔ x ∈ {x ∣ φ}) ↔ (x ∈ A ↔ φ))
6	5	albii 1356	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ {x ∣ φ}) ↔ ∀x(x ∈ A ↔ φ))
7	3, 6	bitri 173	1 ⊢ (A = {x ∣ φ} ↔ ∀x(x ∈ A ↔ φ))

Syntax hints:   ↔ wb 98  ∀wal 1240   = wceq 1242   ∈ wcel 1390  {cab 2023

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033

This theorem is referenced by:  abeq1  2144  abbi2i  2149  abbi2dv  2153  clabel  2160  sbabel  2200  rabid2  2480  ru  2757  sbcabel  2833  dfss2  2928  pwex  3923  dmopab3  4491