Theorem opabidw 5502

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

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

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 2147  ax-9 2155  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5168

This theorem is used by:  rexopabb  5506  ssopab2bw  5526  dmopab  5899  rnopab  5938  funopab  6569  opabiota  6961  fvopab5  7021  f1ompt  7105  ovid  7555  zfrep6OLD  7953  enssdomOLD  8986  omxpenlem  9079  infxpenlem  10019  canthwelem  10662  pospo  18434  2ndcdisj  23685  lgsquadlem1  27619  lgsquadlem2  27620  h2hlm  31464  opabdm  33087  opabrn  33088  fpwrelmap  33207  eulerpartlemgvv  34890  fineqvrep  35643  satfvsucsuc  35947  bj-opelopabid  37942  phpreu  38361  poimirlem26  38398  vvdifopab  39016  brabidgaw  39124  diclspsn  42070  areaquad  44060  sprsymrelf  48398