Theorem opabidw 5504

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

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

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

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 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-opab 5187

This theorem is referenced by:  rexopabb  5508  ssopab2bw  5527  dmopab  5900  rnopab  5939  funopab  6576  opabiota  6966  fvopab5  7024  f1ompt  7106  ovid  7553  zfrep6  7958  enssdom  8996  omxpenlem  9092  infxpenlem  10032  canthwelem  10669  pospo  18360  2ndcdisj  23399  lgsquadlem1  27348  lgsquadlem2  27349  h2hlm  30966  opabdm  32596  opabrn  32597  fpwrelmap  32715  eulerpartlemgvv  34413  fineqvrep  35131  satfvsucsuc  35392  bj-opelopabid  37210  phpreu  37633  poimirlem26  37675  vvdifopab  38283  brabidgaw  38388  diclspsn  41218  areaquad  43215  sprsymrelf  47489