Theorem opabidw 5472

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ⟨cop 4586  {copab 5160

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 2115  ax-9 2123  ax-10 2146  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161

This theorem is referenced by:  rexopabb  5476  ssopab2bw  5495  dmopab  5864  rnopab  5903  funopab  6527  opabiota  6916  fvopab5  6974  f1ompt  7056  ovid  7499  zfrep6  7899  enssdomOLD  8914  omxpenlem  9006  infxpenlem  9923  canthwelem  10561  pospo  18266  2ndcdisj  23400  lgsquadlem1  27347  lgsquadlem2  27348  h2hlm  31055  opabdm  32689  opabrn  32690  fpwrelmap  32812  eulerpartlemgvv  34533  fineqvrep  35270  satfvsucsuc  35559  bj-opelopabid  37392  phpreu  37805  poimirlem26  37847  vvdifopab  38460  brabidgaw  38568  diclspsn  41464  areaquad  43468  sprsymrelf  47751