Theorem abeq2 2050

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 2055 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 1367	. . 3 ⊢ (y ∈ A → ∀x y ∈ A)
2		hbab1 1934	. . 3 ⊢ (y ∈ {x ∣ φ} → ∀x y ∈ {x ∣ φ})
3	1, 2	cleqh 2042	. 2 ⊢ (A = {x ∣ φ} ↔ ∀x(x ∈ A ↔ x ∈ {x ∣ φ}))
4		abid 1933	. . . 4 ⊢ (x ∈ {x ∣ φ} ↔ φ)
5	4	bibi2i 214	. . 3 ⊢ ((x ∈ A ↔ x ∈ {x ∣ φ}) ↔ (x ∈ A ↔ φ))
6	5	albii 1305	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ {x ∣ φ}) ↔ ∀x(x ∈ A ↔ φ))
7	3, 6	bitri 171	1 ⊢ (A = {x ∣ φ} ↔ ∀x(x ∈ A ↔ φ))

Syntax hints:   ↔ wb 96  ∀wal 1281   = wceq 1340   ∈ wcel 1342  {cab 1931

This theorem is referenced by:  abeq1  2051  abbi2i  2056  abbi2dv  2060  clabel  2066  sbabel  2106  rabid2  2370  ru  2643  sbcabel  2720  dfss2  2819

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-5 1282  ax-7 1283  ax-gen 1284  ax-ie1 1329  ax-ie2 1330  ax-8 1344  ax-11 1346  ax-4 1349  ax-17 1367  ax-i9 1371  ax-ial 1376  ax-i5r 1377  ax-ext 1928

This theorem depends on definitions:  df-bi 108  df-nf 1296  df-sb 1586  df-clab 1932  df-cleq 1938  df-clel 1941