Theorem opabidw 5480

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5481 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 5419	. 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		copsexgw 5446	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3	2	bicomd 223	. 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4		df-opab 5163	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
5	1, 3, 4	elab2 3639	1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ⟨cop 4588  {copab 5162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163

This theorem is referenced by:  rexopabb  5484  ssopab2bw  5503  dmopab  5872  rnopab  5911  funopab  6535  opabiota  6924  fvopab5  6983  f1ompt  7065  ovid  7509  zfrep6  7909  enssdomOLD  8926  omxpenlem  9018  infxpenlem  9935  canthwelem  10573  pospo  18278  2ndcdisj  23415  lgsquadlem1  27362  lgsquadlem2  27363  h2hlm  31072  opabdm  32705  opabrn  32706  fpwrelmap  32827  eulerpartlemgvv  34558  fineqvrep  35296  satfvsucsuc  35585  bj-opelopabid  37446  phpreu  37859  poimirlem26  37901  vvdifopab  38520  brabidgaw  38628  diclspsn  41574  areaquad  43577  sprsymrelf  47859