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

Definition df-opab 3819
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 3817 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1242 . . . . . . 7 class 𝑧
72cv 1242 . . . . . . . 8 class 𝑥
83cv 1242 . . . . . . . 8 class 𝑦
97, 8cop 3378 . . . . . . 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  3821  opabbid  3822  nfopab  3825  nfopab1  3826  nfopab2  3827  cbvopab  3828  cbvopab1  3830  cbvopab2  3831  cbvopab1s  3832  cbvopab2v  3834  unopab  3836  opabid  3994  elopab  3995  ssopab2  4012  iunopab  4018  elxpi  4361  rabxp  4380  csbxpg  4421  relopabi  4463  opabbrex  5549  dfoprab2  5552  dmoprab  5585  dfopab2  5815
  Copyright terms: Public domain W3C validator