MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-opab Structured version   Visualization version   GIF version

Definition df-opab 4992
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 (see dfid2 5315 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also (more commonly) called a "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 7558. For example, 𝑅 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ (𝑥 + 1) = 𝑦)} → 3𝑅4 (ex-opab 27989). (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 4991 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1506 . . . . . . 7 class 𝑧
72cv 1506 . . . . . . . 8 class 𝑥
83cv 1506 . . . . . . . 8 class 𝑦
97, 8cop 4447 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1507 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 387 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1742 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1742 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2759 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1507 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  4993  opabbid  4994  nfopab  4997  nfopab1  4998  nfopab2  4999  cbvopab  5000  cbvopab1  5002  cbvopab2  5003  cbvopab1s  5004  cbvopab2v  5006  unopab  5007  opabid  5268  elopab  5269  ssopab2  5287  iunopab  5298  dfid3  5313  elxpi  5429  rabxp  5452  csbxp  5500  ssrel  5507  relopabi  5544  relopabiALT  5545  opabssxpd  5636  cnv0  5839  dfoprab2  7031  dmoprab  7071  dfopab2  7558  brdom7disj  9751  brdom6disj  9752  opabssi  30128  cnvoprabOLD  30208  rnxrn  35088  dropab1  40195  dropab2  40196  csbxpgVD  40644  relopabVD  40651
  Copyright terms: Public domain W3C validator