Theorem opabidw 5534

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5535 with a disjoint variable condition, which does not require ax-13 2375. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2375. (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.

Step	Hyp	Ref	Expression
1		opex 5475	. 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		copsexgw 5501	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3	2	bicomd 223	. 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4		df-opab 5211	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
5	1, 3, 4	elab2 3685	1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1537  ∃wex 1776   ∈ wcel 2106  ⟨cop 4637  {copab 5210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-opab 5211

This theorem is referenced by:  rexopabb  5538  ssopab2bw  5557  dmopab  5929  rnopab  5968  funopab  6603  opabiota  6991  fvopab5  7049  f1ompt  7131  ovid  7574  zfrep6  7978  enssdom  9016  omxpenlem  9112  infxpenlem  10051  canthwelem  10688  pospo  18403  2ndcdisj  23480  lgsquadlem1  27439  lgsquadlem2  27440  h2hlm  31009  opabdm  32631  opabrn  32632  fpwrelmap  32751  eulerpartlemgvv  34358  fineqvrep  35088  satfvsucsuc  35350  bj-opelopabid  37170  phpreu  37591  poimirlem26  37633  vvdifopab  38242  brabidgaw  38347  diclspsn  41177  areaquad  43205  sprsymrelf  47420