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

Definition df-opab 3958
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 3956 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1313 . . . . . . 7 class 𝑧
72cv 1313 . . . . . . . 8 class 𝑥
83cv 1313 . . . . . . . 8 class 𝑦
97, 8cop 3498 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1314 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 103 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1451 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1451 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2101 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1314 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff set class
This definition is referenced by:  opabss  3960  opabbid  3961  nfopab  3964  nfopab1  3965  nfopab2  3966  cbvopab  3967  cbvopab1  3969  cbvopab2  3970  cbvopab1s  3971  cbvopab2v  3973  unopab  3975  opabid  4147  elopab  4148  ssopab2  4165  iunopab  4171  elxpi  4523  rabxp  4544  csbxpg  4588  relopabi  4633  opabbrex  5781  dfoprab2  5784  dmoprab  5818  dfopab2  6053  cnvoprab  6097
  Copyright terms: Public domain W3C validator