Theorem cbvopabv 5181

Description: Rule used to change bound variables in an ordered-pair class abstraction, using implicit substitution. (Contributed by NM, 15-Oct-1996.) Reduce axiom usage. (Revised by GG, 15-Oct-2024.)

Hypothesis

Ref	Expression
cbvopabv.1	⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvopabv	⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}

Distinct variable groups:   𝑥,𝑦,𝑧,𝑤   𝜑,𝑧,𝑤   𝜓,𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥, 𝑦)   𝜓(𝑧, 𝑤)

Proof of Theorem cbvopabv

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq12 4845	. . . . . 6 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ⟨𝑥, 𝑦⟩ = ⟨𝑧, 𝑤⟩)
2	1	eqeq2d 2774	. . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = ⟨𝑥, 𝑦⟩ ↔ 𝑣 = ⟨𝑧, 𝑤⟩))
3		cbvopabv.1	. . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))
4	2, 3	anbi12d 644	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓)))
5	4	cbvex2vw 2075	. . 3 ⊢ (∃𝑥∃𝑦(𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑧∃𝑤(𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓))
6	5	abbii 2830	. 2 ⊢ {𝑣 ∣ ∃𝑥∃𝑦(𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑧∃𝑤(𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓)}
7		df-opab 5171	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦(𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
8		df-opab 5171	. 2 ⊢ {⟨𝑧, 𝑤⟩ ∣ 𝜓} = {𝑣 ∣ ∃𝑧∃𝑤(𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓)}
9	6, 7, 8	3eqtr4i 2796	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569  ∃wex 1811  {cab 2741  ⟨cop 4838  {copab 5170

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-ext 2735

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 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5171

This theorem is used by:  cantnf  9707  infxpen  10106  axdc2  10540  fpwwe2cbv  10728  fpwwecbv  10742  sylow1  19832  bcth  25665  vitali  25949  lgsquadlem3  27724  lgsquad  27725  islnopp  29230  ishpg  29252  hpgbr  29253  elplngid  29275  lnincplng  29277  plngcp  29279  plngrot  29283  nhpmirhp  29291  lnperpexs  29325  trgcopy  29326  trgcopyeu  29328  acopyeu  29357  ragraghl  29361  tgaaddcpbllem2  29365  tgaaddcpbl2  29368  angmgmaddeu1  29394  tgasa1  29418  prlnghpg  29439  prlngmo  29447  axcontlem1  29557  tgextahpl  33084  tgextancgra  33089  constrext2chn  34447  eulerpartlemgvv  35064  eulerpart  35070  cvmlift2lem13  36204  pellex  43988  aomclem8  44209  sprsymrelf  48722