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

Theorem opabidw 5479
Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5480 with a disjoint variable condition, which does not require ax-13 2370. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2370. (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 5419 . 2 𝑥, 𝑦⟩ ∈ V
2 copsexgw 5445 . . 3 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
32bicomd 222 . 2 (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4 df-opab 5166 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
51, 3, 4elab2 3632 1 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  cop 4590  {copab 5165
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2707  ax-sep 5254  ax-nul 5261  ax-pr 5382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5166
This theorem is referenced by:  rexopabb  5483  ssopab2bw  5502  dmopab  5869  rnopab  5907  funopab  6533  opabiota  6921  fvopab5  6977  f1ompt  7055  ovid  7492  zfrep6  7883  enssdom  8913  omxpenlem  9013  infxpenlem  9945  canthwelem  10582  pospo  18226  2ndcdisj  22791  lgsquadlem1  26712  lgsquadlem2  26713  h2hlm  29808  opabdm  31416  opabrn  31417  fpwrelmap  31533  eulerpartlemgvv  32845  fineqvrep  33565  satfvsucsuc  33828  bj-opelopabid  35625  phpreu  36029  poimirlem26  36071  vvdifopab  36687  brabidgaw  36793  diclspsn  39624  areaquad  41488  sprsymrelf  45619
  Copyright terms: Public domain W3C validator