Theorem cleqab 1174

Description: Equality of a class variable and an class abstraction. Theorem 5.1 of [Quine] p. 34. This theorem is useful for converting expressions with class abstractions to expressions with class variables. Note that cleq2ab 1179 and its relatives are among those useful for converting theorems with class variables to equivalent theorems with wff variables, by first substituting an 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. An example is the conversion of zfaus 1480 to inex1 1697 (look at the instance of zfaus 1480 that occurs in the proof of inex1 1697). Conversely, to convert a theorem with a class variable A to one with φ, we substitute {x∣φ} for A throughout and simplify. An example is cp 3547, which derives a formula containing wff variables from substitution instances of the class variables in its equivalent formulation cplem2 3546.

Assertion

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

Distinct variable group(s):   x,A

Proof of Theorem cleqab

Step	Hyp	Ref	Expression
1		ax-17 925	. . 3 ⊢ (y ∈ A → ∀x y ∈ A)
2		hbab1 1095	. . 3 ⊢ (y ∈ {x∣φ} → ∀x y ∈ {x∣φ})
3	1, 2	cleqf 1167	. 2 ⊢ (A = {x∣φ} ↔ ∀x(x ∈ A ↔ x ∈ {x∣φ}))
4		abid 1094	. . . 4 ⊢ (x ∈ {x∣φ} ↔ φ)
5	4	bibi2i 460	. . 3 ⊢ ((x ∈ A ↔ x ∈ {x∣φ}) ↔ (x ∈ A ↔ φ))
6	5	bial 695	. 2 ⊢ (∀x(x ∈ A ↔ x ∈ {x∣φ}) ↔ ∀x(x ∈ A ↔ φ))
7	3, 6	bitr 151	1 ⊢ (A = {x∣φ} ↔ ∀x(x ∈ A ↔ φ))

Syntax hints:   ↔ wb 127  ∀wal 672  {cab 1090   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  cleqabr 1175  biabri 1180  biabrdv 1184  sbabel 1189  rabid2 1309  ru 1437  zfrep4 1479  dfss2 1497  ssequn1 1628  pwex 1806  dmopab2 2541  funimaexg 2715

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099

metamath.org