Theorem opabidw 5437

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

Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ⟨cop 4567  {copab 5136

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137

This theorem is referenced by:  rexopabb  5441  ssopab2bw  5460  dmopab  5824  rnopab  5863  funopab  6469  opabiota  6851  fvopab5  6907  f1ompt  6985  ovid  7414  zfrep6  7797  enssdom  8765  omxpenlem  8860  infxpenlem  9769  canthwelem  10406  pospo  18063  2ndcdisj  22607  lgsquadlem1  26528  lgsquadlem2  26529  h2hlm  29342  opabdm  30951  opabrn  30952  fpwrelmap  31068  eulerpartlemgvv  32343  fineqvrep  33064  satfvsucsuc  33327  bj-opelopabid  35358  phpreu  35761  poimirlem26  35803  vvdifopab  36399  brabidgaw  36495  diclspsn  39208  areaquad  41047  sprsymrelf  44947