Theorem opabidw 5467

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

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

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-opab 5155

This theorem is referenced by:  rexopabb  5471  ssopab2bw  5490  dmopab  5858  rnopab  5896  funopab  6517  opabiota  6905  fvopab5  6963  f1ompt  7045  ovid  7490  zfrep6  7890  enssdom  8902  omxpenlem  8995  infxpenlem  9907  canthwelem  10544  pospo  18249  2ndcdisj  23341  lgsquadlem1  27289  lgsquadlem2  27290  h2hlm  30924  opabdm  32556  opabrn  32557  fpwrelmap  32676  eulerpartlemgvv  34344  fineqvrep  35070  satfvsucsuc  35342  bj-opelopabid  37165  phpreu  37588  poimirlem26  37630  vvdifopab  38239  brabidgaw  38337  diclspsn  41177  areaquad  43193  sprsymrelf  47483