Theorem opabidw 5462

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5463 with a disjoint variable condition, which does not require ax-13 2372. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2372. (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 5402	. 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		copsexgw 5428	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3	2	bicomd 223	. 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4		df-opab 5152	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
5	1, 3, 4	elab2 3633	1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ⟨cop 4579  {copab 5151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-opab 5152

This theorem is referenced by:  rexopabb  5466  ssopab2bw  5485  dmopab  5854  rnopab  5893  funopab  6516  opabiota  6904  fvopab5  6962  f1ompt  7044  ovid  7487  zfrep6  7887  enssdom  8899  omxpenlem  8991  infxpenlem  9904  canthwelem  10541  pospo  18249  2ndcdisj  23371  lgsquadlem1  27318  lgsquadlem2  27319  h2hlm  30960  opabdm  32594  opabrn  32595  fpwrelmap  32716  eulerpartlemgvv  34389  fineqvrep  35137  satfvsucsuc  35409  bj-opelopabid  37231  phpreu  37654  poimirlem26  37696  vvdifopab  38307  brabidgaw  38407  diclspsn  41303  areaquad  43319  sprsymrelf  47605