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

Definition df-opab 3816
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 3814 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1242 . . . . . . 7 class 𝑧
72cv 1242 . . . . . . . 8 class 𝑥
83cv 1242 . . . . . . . 8 class 𝑦
97, 8cop 3375 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1243 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 97 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1381 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1381 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2026 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1243 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff set class
This definition is referenced by:  opabss  3818  opabbid  3819  nfopab  3822  nfopab1  3823  nfopab2  3824  cbvopab  3825  cbvopab1  3827  cbvopab2  3828  cbvopab1s  3829  cbvopab2v  3831  unopab  3833  opabid  3991  elopab  3992  ssopab2  4009  iunopab  4015  elxpi  4339  rabxp  4358  csbxpg  4399  relopabi  4441  opabbrex  5527  dfoprab2  5530  dmoprab  5563  dfopab2  5793
  Copyright terms: Public domain W3C validator