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 5208
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 does not require it (see dfid2 5574 for a case where they are not distinct). The brace notation is called "class abstraction" by Quine; it is also called "class builder" in the literature. An alternate definition using no existential quantifiers is shown by dfopab2 8058. An example is given by ex-opab 30362. (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 5207 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1533 . . . . . . 7 class 𝑧
72cv 1533 . . . . . . . 8 class 𝑥
83cv 1533 . . . . . . . 8 class 𝑦
97, 8cop 4629 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1534 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 394 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1774 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1774 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2703 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1534 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  5209  opabbid  5210  opabbidv  5211  nfopabd  5213  nfopab1  5215  nfopab2  5216  cbvopab  5217  cbvopabv  5218  cbvopab1  5220  cbvopab1g  5221  cbvopab2  5222  cbvopab1s  5223  cbvopab1v  5224  cbvopab2v  5226  unopab  5227  opabidw  5522  opabid  5523  elopabw  5524  ssopab2  5544  iunopab  5557  iunopabOLD  5558  dfid2  5574  dfid3  5575  elxpi  5696  opabssxpd  5721  rabxp  5722  csbxp  5773  ssrelOLD  5781  relopabi  5820  relopabiALT  5821  cnv0  6144  dfoprab2  7475  dmoprab  7519  dfopab2  8058  brdom7disj  10565  brdom6disj  10566  opabssi  32533  cnvoprabOLD  32634  bj-dfid2ALT  36785  rnxrn  38109  dropab1  44158  dropab2  44159  csbxpgVD  44607  relopabVD  44614
  Copyright terms: Public domain W3C validator