Theorem opabidw 5528

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

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ⟨cop 4631  {copab 5204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-opab 5205

This theorem is referenced by:  rexopabb  5532  ssopab2bw  5551  dmopab  5925  rnopab  5964  funopab  6600  opabiota  6990  fvopab5  7048  f1ompt  7130  ovid  7575  zfrep6  7980  enssdom  9018  omxpenlem  9114  infxpenlem  10054  canthwelem  10691  pospo  18391  2ndcdisj  23465  lgsquadlem1  27425  lgsquadlem2  27426  h2hlm  31000  opabdm  32624  opabrn  32625  fpwrelmap  32745  eulerpartlemgvv  34379  fineqvrep  35110  satfvsucsuc  35371  bj-opelopabid  37189  phpreu  37612  poimirlem26  37654  vvdifopab  38262  brabidgaw  38367  diclspsn  41197  areaquad  43233  sprsymrelf  47487