Theorem opabidw 5523

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

Syntax hints:   ↔ wb 205   ∧ wa 394   = wceq 1539  ∃wex 1779   ∈ wcel 2104  ⟨cop 4633  {copab 5209

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-opab 5210

This theorem is referenced by:  rexopabb  5527  ssopab2bw  5546  dmopab  5914  rnopab  5952  funopab  6582  opabiota  6973  fvopab5  7029  f1ompt  7111  ovid  7551  zfrep6  7943  enssdom  8975  omxpenlem  9075  infxpenlem  10010  canthwelem  10647  pospo  18302  2ndcdisj  23180  lgsquadlem1  27119  lgsquadlem2  27120  h2hlm  30500  opabdm  32107  opabrn  32108  fpwrelmap  32225  eulerpartlemgvv  33673  fineqvrep  34393  satfvsucsuc  34654  bj-opelopabid  36371  phpreu  36775  poimirlem26  36817  vvdifopab  37431  brabidgaw  37537  diclspsn  40368  areaquad  42267  sprsymrelf  46461