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

Theorem opabidw 5437
Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5438 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 14-Apr-1995.) (Revised by Gino Giotto, 26-Jan-2024.)
Assertion
Ref Expression
opabidw (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Distinct variable group:   𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem opabidw
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 opex 5379 . 2 𝑥, 𝑦⟩ ∈ V
2 copsexgw 5404 . . 3 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
32bicomd 222 . 2 (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4 df-opab 5137 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
51, 3, 4elab2 3613 1 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1539  wex 1782  wcel 2106  cop 4567  {copab 5136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137
This theorem is referenced by:  rexopabb  5441  ssopab2bw  5460  dmopab  5824  rnopab  5863  funopab  6469  opabiota  6851  fvopab5  6907  f1ompt  6985  ovid  7414  zfrep6  7797  enssdom  8765  omxpenlem  8860  infxpenlem  9769  canthwelem  10406  pospo  18063  2ndcdisj  22607  lgsquadlem1  26528  lgsquadlem2  26529  h2hlm  29342  opabdm  30951  opabrn  30952  fpwrelmap  31068  eulerpartlemgvv  32343  fineqvrep  33064  satfvsucsuc  33327  bj-opelopabid  35358  phpreu  35761  poimirlem26  35803  vvdifopab  36399  brabidgaw  36495  diclspsn  39208  areaquad  41047  sprsymrelf  44947
  Copyright terms: Public domain W3C validator