Theorem opabidw 5511

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ⟨cop 4598  {copab 5176

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-pr 5407

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5177

This theorem is used by:  rexopabb  5515  ssopab2bw  5535  dmopab  5908  rnopab  5947  funopab  6575  opabiota  6967  fvopab5  7027  f1ompt  7110  ovid  7557  zfrep6OLD  7954  enssdomOLD  8976  omxpenlem  9068  infxpenlem  10008  canthwelem  10645  pospo  18409  2ndcdisj  23628  lgsquadlem1  27559  lgsquadlem2  27560  h2hlm  31347  opabdm  32971  opabrn  32972  fpwrelmap  33093  eulerpartlemgvv  34779  fineqvrep  35539  satfvsucsuc  35869  bj-opelopabid  37863  phpreu  38287  poimirlem26  38329  vvdifopab  38946  brabidgaw  39054  diclspsn  42000  areaquad  43975  sprsymrelf  48276