ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-opab GIF version

Definition df-opab 3908
Description: Define the class abstraction of a collection of ordered pairs. Definition 3.3 of [Monk1] p. 34. Usually 𝑥 and 𝑦 are distinct, although the definition doesn't strictly require it. The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
df-opab {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Distinct variable groups:   𝑥,𝑧   𝑦,𝑧   𝜑,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Definition df-opab
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
41, 2, 3copab 3906 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1289 . . . . . . 7 class 𝑧
72cv 1289 . . . . . . . 8 class 𝑥
83cv 1289 . . . . . . . 8 class 𝑦
97, 8cop 3455 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1290 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 103 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1427 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1427 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2075 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1290 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff set class
This definition is referenced by:  opabss  3910  opabbid  3911  nfopab  3914  nfopab1  3915  nfopab2  3916  cbvopab  3917  cbvopab1  3919  cbvopab2  3920  cbvopab1s  3921  cbvopab2v  3923  unopab  3925  opabid  4095  elopab  4096  ssopab2  4113  iunopab  4119  elxpi  4470  rabxp  4490  csbxpg  4534  relopabi  4578  opabbrex  5709  dfoprab2  5712  dmoprab  5745  dfopab2  5975  cnvoprab  6015
  Copyright terms: Public domain W3C validator