Theorem opabidw 5498

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ⟨cop 4590  {copab 5167

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168

This theorem is used by:  rexopabb  5502  ssopab2bw  5522  dmopab  5897  rnopab  5936  funopab  6575  opabiota  6967  fvopab5  7027  f1ompt  7111  ovid  7561  zfrep6OLD  7967  enssdomOLD  9004  omxpenlem  9097  infxpenlem  10092  canthwelem  10735  pospo  18517  2ndcdisj  23775  lgsquadlem1  27707  lgsquadlem2  27708  h2hlm  31582  opabdm  33205  opabrn  33206  fpwrelmap  33325  eulerpartlemgvv  35008  fineqvrep  35782  satfvsucsuc  36130  bj-opelopabid  38108  phpreu  38527  poimirlem26  38564  vvdifopab  39197  brabidgaw  39305  diclspsn  42251  areaquad  44217  sprsymrelf  48576