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

Theorem opabid 5208
Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. (Contributed by NM, 14-Apr-1995.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
opabid (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Proof of Theorem opabid
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 opex 5153 . 2 𝑥, 𝑦⟩ ∈ V
2 copsexg 5176 . . 3 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
32bicomd 215 . 2 (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4 df-opab 4936 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
51, 3, 4elab2 3575 1 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386   = wceq 1656  wex 1878  wcel 2164  cop 4403  {copab 4935
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-opab 4936
This theorem is referenced by:  opelopabsb  5211  ssopab2b  5228  dmopab  5567  rnopab  5603  funopab  6158  opabiota  6508  fvopab5  6558  f1ompt  6630  ovid  7037  zfrep6  7396  enssdom  8247  omxpenlem  8330  infxpenlem  9149  canthwelem  9787  pospo  17326  2ndcdisj  21630  lgsquadlem1  25518  lgsquadlem2  25519  h2hlm  28381  opabdm  29959  opabrn  29960  fpwrelmap  30045  eulerpartlemgvv  30972  phpreu  33929  poimirlem26  33972  vvdifopab  34571  brabidga  34669  diclspsn  37262  areaquad  38637  sprsymrelf  42585
  Copyright terms: Public domain W3C validator