Theorem cbvabv 2799

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2801 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2158 and ax-13 2370. (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 2101	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
3		df-clab 2708	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
4		df-clab 2708	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
6	5	eqriv 2726	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721

This theorem is referenced by:  cbvrabv  3405  cbvsbcvw  3776  difjust  3905  unjust  3907  injust  3909  uniiunlem  4038  dfif3  4491  pwjust  4552  snjust  4576  intab  4928  intabs  5288  iotajust  6437  cbviotavw  6446  frrlem1  8219  fsetprcnex  8789  sbth  9014  sbthfi  9113  cardprc  9876  iunfictbso  10008  aceq3lem  10014  isf33lem  10260  axdc3  10348  axdclem  10413  axdc  10415  genpv  10893  ltexpri  10937  recexpr  10945  supsr  11006  hashf1lem2  14363  cvbtrcl  14899  mertens  15793  4sq  16876  symgval  19250  nosupcbv  27612  nosupdm  27614  noinfcbv  27627  noinfdm  27629  addsval2  27875  addscut  27890  addsunif  27914  addsasslem1  27915  addsasslem2  27916  mulsval2lem  28018  mulsunif2  28078  precsexlemcbv  28113  isuhgr  29005  isushgr  29006  isupgr  29029  isumgr  29040  isuspgr  29097  isusgr  29098  isconngr  30133  isconngr1  30134  dispcmp  33832  eulerpart  34356  ballotlemfmpn  34469  bnj66  34833  bnj1234  34986  setinds2regs  35072  tz9.1regs  35073  subfacp1lem6  35168  subfacp1  35169  dfon2lem3  35769  dfon2lem7  35773  cbvsbcvw2  36214  cbvixpvw2  36229  bj-gabeqis  36922  f1omptsn  37321  rdgssun  37362  ismblfin  37651  glbconxN  39367  sticksstones15  42144  eldioph3  42749  diophrex  42758  cbvcllem  43592  cbvrabv2w  45116  ssfiunibd  45301  aiotajust  47078