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 5096
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 5431 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 7736. An example is given by ex-opab 28221. (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 5095 . 2 class {⟨𝑥, 𝑦⟩ ∣ 𝜑}
5 vz . . . . . . . 8 setvar 𝑧
65cv 1537 . . . . . . 7 class 𝑧
72cv 1537 . . . . . . . 8 class 𝑥
83cv 1537 . . . . . . . 8 class 𝑦
97, 8cop 4534 . . . . . . 7 class 𝑥, 𝑦
106, 9wceq 1538 . . . . . 6 wff 𝑧 = ⟨𝑥, 𝑦
1110, 1wa 399 . . . . 5 wff (𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1211, 3wex 1781 . . . 4 wff 𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1312, 2wex 1781 . . 3 wff 𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)
1413, 5cab 2779 . 2 class {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
154, 14wceq 1538 1 wff {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
Colors of variables: wff setvar class
This definition is referenced by:  opabss  5097  opabbid  5098  nfopab  5101  nfopab1  5102  nfopab2  5103  cbvopab  5104  cbvopab1  5106  cbvopab1g  5107  cbvopab2  5108  cbvopab1s  5109  cbvopab2v  5111  unopab  5112  opabidw  5380  opabid  5381  elopab  5382  ssopab2  5401  iunopab  5414  dfid3  5430  elxpi  5545  rabxp  5568  csbxp  5618  ssrel  5625  relopabi  5662  relopabiALT  5663  opabssxpd  5757  cnv0  5970  dfoprab2  7195  dmoprab  7238  dfopab2  7736  brdom7disj  9946  brdom6disj  9947  opabssi  30381  cnvoprabOLD  30486  rnxrn  35805  dropab1  41144  dropab2  41145  csbxpgVD  41593  relopabVD  41600
  Copyright terms: Public domain W3C validator