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 2370. (Contributed by NM, 14-Apr-1995.) Avoid ax-13 2370. (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 5419	. 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		copsexgw 5445	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3	2	bicomd 223	. 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4		df-opab 5165	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
5	1, 3, 4	elab2 3646	1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ⟨cop 4591  {copab 5164

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5165

This theorem is referenced by:  rexopabb  5483  ssopab2bw  5502  dmopab  5869  rnopab  5907  funopab  6535  opabiota  6925  fvopab5  6983  f1ompt  7065  ovid  7510  zfrep6  7913  enssdom  8925  omxpenlem  9019  infxpenlem  9942  canthwelem  10579  pospo  18284  2ndcdisj  23376  lgsquadlem1  27324  lgsquadlem2  27325  h2hlm  30959  opabdm  32589  opabrn  32590  fpwrelmap  32706  eulerpartlemgvv  34360  fineqvrep  35078  satfvsucsuc  35345  bj-opelopabid  37168  phpreu  37591  poimirlem26  37633  vvdifopab  38242  brabidgaw  38340  diclspsn  41181  areaquad  43198  sprsymrelf  47489