Theorem opabidw 5406

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5407 with a disjoint variable condition, which does not require ax-13 2371. (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 5348	. 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		copsexgw 5373	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3	2	bicomd 226	. 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4		df-opab 5116	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
5	1, 3, 4	elab2 3591	1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1543  ∃wex 1787   ∈ wcel 2110  ⟨cop 4547  {copab 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-opab 5116

This theorem is referenced by:  rexopabb  5409  ssopab2bw  5428  dmopab  5784  rnopab  5823  funopab  6415  opabiota  6794  fvopab5  6850  f1ompt  6928  ovid  7350  zfrep6  7728  enssdom  8653  omxpenlem  8746  infxpenlem  9627  canthwelem  10264  pospo  17851  2ndcdisj  22353  lgsquadlem1  26261  lgsquadlem2  26262  h2hlm  29061  opabdm  30670  opabrn  30671  fpwrelmap  30788  eulerpartlemgvv  32055  fineqvrep  32777  satfvsucsuc  33040  bj-opelopabid  35093  phpreu  35498  poimirlem26  35540  vvdifopab  36136  brabidgaw  36232  diclspsn  38945  areaquad  40750  sprsymrelf  44620