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

Theorem opabidw 5378
 Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5379 with a disjoint variable condition, which does not require ax-13 2379. (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 5322 . 2 𝑥, 𝑦⟩ ∈ V
2 copsexgw 5347 . . 3 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
32bicomd 226 . 2 (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4 df-opab 5094 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
51, 3, 4elab2 3618 1 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ⟨cop 4531  {copab 5093 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5168  ax-nul 5175  ax-pr 5296 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-opab 5094 This theorem is referenced by:  rexopabb  5381  opelopabsb  5383  ssopab2bw  5400  dmopab  5749  rnopab  5791  funopab  6362  opabiota  6726  fvopab5  6782  f1ompt  6857  ovid  7276  zfrep6  7645  enssdom  8524  omxpenlem  8608  infxpenlem  9431  canthwelem  10068  pospo  17582  2ndcdisj  22075  lgsquadlem1  25978  lgsquadlem2  25979  h2hlm  28777  opabdm  30389  opabrn  30390  fpwrelmap  30509  eulerpartlemgvv  31780  satfvsucsuc  32761  bj-opelopabid  34642  phpreu  35081  poimirlem26  35123  vvdifopab  35721  brabidgaw  35817  diclspsn  38530  areaquad  40230  sprsymrelf  44073
 Copyright terms: Public domain W3C validator