Theorem opabidw 5470

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

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

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-opab 5159

This theorem is referenced by:  rexopabb  5474  ssopab2bw  5493  dmopab  5862  rnopab  5901  funopab  6525  opabiota  6914  fvopab5  6972  f1ompt  7054  ovid  7497  zfrep6  7897  enssdomOLD  8912  omxpenlem  9004  infxpenlem  9921  canthwelem  10559  pospo  18264  2ndcdisj  23398  lgsquadlem1  27345  lgsquadlem2  27346  h2hlm  31004  opabdm  32638  opabrn  32639  fpwrelmap  32761  eulerpartlemgvv  34482  fineqvrep  35219  satfvsucsuc  35508  bj-opelopabid  37331  phpreu  37744  poimirlem26  37786  vvdifopab  38397  brabidgaw  38497  diclspsn  41393  areaquad  43400  sprsymrelf  47683