Theorem opabidw 5508

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

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ⟨cop 4595  {copab 5173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174

This theorem is referenced by:  rexopabb  5512  ssopab2bw  5532  dmopab  5905  rnopab  5944  funopab  6571  opabiota  6963  fvopab5  7023  f1ompt  7106  ovid  7551  zfrep6OLD  7948  enssdomOLD  8970  omxpenlem  9062  infxpenlem  9993  canthwelem  10630  pospo  18394  2ndcdisj  23613  lgsquadlem1  27544  lgsquadlem2  27545  h2hlm  31332  opabdm  32956  opabrn  32957  fpwrelmap  33078  eulerpartlemgvv  34766  fineqvrep  35527  satfvsucsuc  35857  bj-opelopabid  37851  phpreu  38275  poimirlem26  38317  vvdifopab  38934  brabidgaw  39042  diclspsn  41988  areaquad  43963  sprsymrelf  48264