Theorem cbvopabv 5184

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 4840	. . . . . 6 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ⟨𝑥, 𝑦⟩ = ⟨𝑧, 𝑤⟩)
2	1	eqeq2d 2774	. . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = ⟨𝑥, 𝑦⟩ ↔ 𝑣 = ⟨𝑧, 𝑤⟩))
3		cbvopabv.1	. . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝜑 ↔ 𝜓))
4	2, 3	anbi12d 643	. . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ (𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓)))
5	4	cbvex2vw 2071	. . 3 ⊢ (∃𝑥∃𝑦(𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) ↔ ∃𝑧∃𝑤(𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓))
6	5	abbii 2830	. 2 ⊢ {𝑣 ∣ ∃𝑥∃𝑦(𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} = {𝑣 ∣ ∃𝑧∃𝑤(𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓)}
7		df-opab 5174	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑣 ∣ ∃𝑥∃𝑦(𝑣 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)}
8		df-opab 5174	. 2 ⊢ {⟨𝑧, 𝑤⟩ ∣ 𝜓} = {𝑣 ∣ ∃𝑧∃𝑤(𝑣 = ⟨𝑧, 𝑤⟩ ∧ 𝜓)}
9	6, 7, 8	3eqtr4i 2796	1 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} = {⟨𝑧, 𝑤⟩ ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809  {cab 2741  ⟨cop 4595  {copab 5173

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5174

This theorem is used by:  cantnf  9658  infxpen  10003  axdc2  10437  fpwwe2cbv  10619  fpwwecbv  10633  sylow1  19677  bcth  25497  vitali  25781  lgsquadlem3  27555  lgsquad  27556  islnopp  29029  ishpg  29050  hpgbr  29051  elplngid  29073  lnincplng  29075  plngcp  29077  plngrot  29081  nhpmirhp  29089  lnperpexs  29123  trgcopy  29124  trgcopyeu  29126  acopyeu  29154  ragraghl  29158  tgasa1  29184  prlnghpg  29205  prlngmo  29213  axcontlem1  29323  constrext2chn  34158  eulerpartlemgvv  34775  eulerpart  34781  cvmlift2lem13  35815  pellex  43590  aomclem8  43816  sprsymrelf  48272