Theorem opabidw 5501

Description: The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 5502 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 5435	. 2 ⊢ ⟨𝑥, 𝑦⟩ ∈ V
2		copsexgw 5463	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝜑 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)))
3	2	bicomd 226	. 2 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ 𝜑))
4		df-opab 5170	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
5	1, 3, 4	elab2 3638	1 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ 𝜑)

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2146  ⟨cop 4837  {copab 5169

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-pr 5394

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-opab 5170

This theorem is used by:  rexopabb  5505  ssopab2bw  5525  dmopab  5901  rnopab  5940  funopab  6583  opabiota  6975  fvopab5  7035  f1ompt  7119  ovid  7568  zfrep6OLD  7974  enssdomOLD  9015  omxpenlem  9108  infxpenlem  10102  canthwelem  10745  pospo  18529  2ndcdisj  23787  lgsquadlem1  27719  lgsquadlem2  27720  h2hlm  31594  opabdm  33259  opabrn  33260  fpwrelmap  33378  eulerpartlemgvv  35061  fwfffun  35770  rankse  35802  fineqvrep  35853  satfvsucsuc  36251  bj-opelopabid  38248  phpreu  38667  poimirlem26  38704  vvdifopab  39337  brabidgaw  39445  diclspsn  42391  areaquad  44358  sprsymrelf  48716