Theorem opabidw 5479

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5480 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 5416	. 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		copsexgw 5443	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3	2	bicomd 223	. 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4		df-opab 5148	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
5	1, 3, 4	elab2 3625	1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ⟨cop 4573  {copab 5147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148

This theorem is referenced by:  rexopabb  5483  ssopab2bw  5502  dmopab  5870  rnopab  5909  funopab  6533  opabiota  6922  fvopab5  6981  f1ompt  7063  ovid  7508  zfrep6OLD  7908  enssdomOLD  8924  omxpenlem  9016  infxpenlem  9935  canthwelem  10573  pospo  18309  2ndcdisj  23421  lgsquadlem1  27343  lgsquadlem2  27344  h2hlm  31051  opabdm  32684  opabrn  32685  fpwrelmap  32806  eulerpartlemgvv  34520  fineqvrep  35258  satfvsucsuc  35547  bj-opelopabid  37501  phpreu  37925  poimirlem26  37967  vvdifopab  38586  brabidgaw  38694  diclspsn  41640  areaquad  43644  sprsymrelf  47955