Theorem cbvabv 2804

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2806 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2162 and ax-13 2374. (Revised by Steven Nguyen, 4-Dec-2022.)

Hypothesis

Ref	Expression
cbvabv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvabv	⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

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

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvabv

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cbvabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	cbvsbv 2105	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
3		df-clab 2713	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
4		df-clab 2713	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
6	5	eqriv 2731	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2067   ∈ wcel 2113  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726

This theorem is referenced by:  cbvrabv  3407  cbvsbcvw  3772  difjust  3901  unjust  3903  injust  3905  uniiunlem  4037  dfif3  4492  pwjust  4553  snjust  4577  intab  4931  intabs  5292  iotajust  6445  cbviotavw  6454  frrlem1  8226  fsetprcnex  8797  sbth  9023  sbthfi  9121  cardprc  9890  iunfictbso  10022  aceq3lem  10028  isf33lem  10274  axdc3  10362  axdclem  10427  axdc  10429  genpv  10908  ltexpri  10952  recexpr  10960  supsr  11021  hashf1lem2  14377  cvbtrcl  14913  mertens  15807  4sq  16890  symgval  19298  nosupcbv  27668  nosupdm  27670  noinfcbv  27683  noinfdm  27685  addsval2  27933  addscut  27948  addsunif  27972  addsasslem1  27973  addsasslem2  27974  mulsval2lem  28079  mulsunif2  28139  precsexlemcbv  28174  isuhgr  29082  isushgr  29083  isupgr  29106  isumgr  29117  isuspgr  29174  isusgr  29175  isconngr  30213  isconngr1  30214  dispcmp  33965  eulerpart  34488  ballotlemfmpn  34601  bnj66  34965  bnj1234  35118  setinds2regs  35236  tz9.1regs  35239  subfacp1lem6  35328  subfacp1  35329  dfon2lem3  35926  dfon2lem7  35930  cbvsbcvw2  36373  cbvixpvw2  36388  bj-gabeqis  37082  f1omptsn  37481  rdgssun  37522  ismblfin  37801  glbconxN  39577  sticksstones15  42354  eldioph3  42950  diophrex  42959  cbvcllem  43792  cbvrabv2w  45314  ssfiunibd  45499  aiotajust  47272