Theorem opabidw 5509

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ⟨cop 4600  {copab 5177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-opab 5178

This theorem is referenced by:  rexopabb  5513  ssopab2bw  5533  dmopab  5906  rnopab  5945  funopab  6572  opabiota  6964  fvopab5  7024  f1ompt  7107  ovid  7552  zfrep6OLD  7952  enssdomOLD  8974  omxpenlem  9066  infxpenlem  9997  canthwelem  10635  pospo  18399  2ndcdisj  23582  lgsquadlem1  27510  lgsquadlem2  27511  h2hlm  31273  opabdm  32897  opabrn  32898  fpwrelmap  33019  eulerpartlemgvv  34711  fineqvrep  35450  satfvsucsuc  35756  bj-opelopabid  37719  phpreu  38143  poimirlem26  38185  vvdifopab  38804  brabidgaw  38912  diclspsn  41858  areaquad  43835  sprsymrelf  48133