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

Definition df-opab 3847
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 3845 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1258 . . . . . . 7 class 𝑧
72cv 1258 . . . . . . . 8 class 𝑥
83cv 1258 . . . . . . . 8 class 𝑦
97, 8cop 3406 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1259 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 101 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1397 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1397 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2042 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1259 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff set class
This definition is referenced by:  opabss  3849  opabbid  3850  nfopab  3853  nfopab1  3854  nfopab2  3855  cbvopab  3856  cbvopab1  3858  cbvopab2  3859  cbvopab1s  3860  cbvopab2v  3862  unopab  3864  opabid  4022  elopab  4023  ssopab2  4040  iunopab  4046  elxpi  4389  rabxp  4408  csbxpg  4449  relopabi  4491  opabbrex  5577  dfoprab2  5580  dmoprab  5613  dfopab2  5843  cnvoprab  5883
  Copyright terms: Public domain W3C validator