Theorem opabidw 5431

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

Syntax hints:   ↔ wb 205   ∧ wa 395   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ⟨cop 4564  {copab 5132

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133

This theorem is referenced by:  rexopabb  5434  ssopab2bw  5453  dmopab  5813  rnopab  5852  funopab  6453  opabiota  6833  fvopab5  6889  f1ompt  6967  ovid  7392  zfrep6  7771  enssdom  8720  omxpenlem  8813  infxpenlem  9700  canthwelem  10337  pospo  17978  2ndcdisj  22515  lgsquadlem1  26433  lgsquadlem2  26434  h2hlm  29243  opabdm  30852  opabrn  30853  fpwrelmap  30970  eulerpartlemgvv  32243  fineqvrep  32964  satfvsucsuc  33227  bj-opelopabid  35285  phpreu  35688  poimirlem26  35730  vvdifopab  36326  brabidgaw  36422  diclspsn  39135  areaquad  40963  sprsymrelf  44835