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

Theorem opabidw 5511
Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5512 with a disjoint variable condition, which does not require ax-13 2407. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2407. (Revised by GG, 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 5448 . 2 𝑥, 𝑦⟩ ∈ V
2 copsexgw 5475 . . 3 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
32bicomd 226 . 2 (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4 df-opab 5177 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
51, 3, 4elab2 3644 1 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  wb 209  wa 401   = wceq 1570  wex 1812  wcel 2146  cop 4598  {copab 5176
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-pr 5407
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5177
This theorem is used by:  rexopabb  5515  ssopab2bw  5535  dmopab  5908  rnopab  5947  funopab  6575  opabiota  6967  fvopab5  7027  f1ompt  7110  ovid  7557  zfrep6OLD  7954  enssdomOLD  8976  omxpenlem  9068  infxpenlem  10008  canthwelem  10645  pospo  18409  2ndcdisj  23628  lgsquadlem1  27559  lgsquadlem2  27560  h2hlm  31347  opabdm  32971  opabrn  32972  fpwrelmap  33093  eulerpartlemgvv  34779  fineqvrep  35539  satfvsucsuc  35869  bj-opelopabid  37863  phpreu  38287  poimirlem26  38329  vvdifopab  38946  brabidgaw  39054  diclspsn  42000  areaquad  43975  sprsymrelf  48276
  Copyright terms: Public domain W3C validator