Theorem opabidw 5466

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

Syntax hints:   ↔ wb 207   ∧ wa 396   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ⟨cop 4561  {copab 5134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-opab 5135

This theorem is referenced by:  rexopabb  5470  ssopab2bw  5489  dmopab  5857  rnopab  5896  funopab  6520  opabiota  6909  fvopab5  6969  f1ompt  7052  ovid  7497  zfrep6OLD  7897  enssdomOLD  8914  omxpenlem  9006  infxpenlem  9926  canthwelem  10564  pospo  18300  2ndcdisj  23439  lgsquadlem1  27361  lgsquadlem2  27362  h2hlm  31069  opabdm  32703  opabrn  32704  fpwrelmap  32825  eulerpartlemgvv  34560  fineqvrep  35295  satfvsucsuc  35593  bj-opelopabid  37547  phpreu  37971  poimirlem26  38013  vvdifopab  38632  brabidgaw  38740  diclspsn  41686  areaquad  43661  sprsymrelf  47970