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  3416  cbvsbcvw  3787  difjust  3916  unjust  3918  injust  3920  uniiunlem  4050  dfif3  4503  pwjust  4564  snjust  4588  intab  4942  intabs  5304  iotajust  6463  cbviotavw  6472  frrlem1  8265  fsetprcnex  8835  sbth  9061  sbthfi  9163  cardprc  9933  iunfictbso  10067  aceq3lem  10073  isf33lem  10319  axdc3  10407  axdclem  10472  axdc  10474  genpv  10952  ltexpri  10996  recexpr  11004  supsr  11065  hashf1lem2  14421  cvbtrcl  14958  mertens  15852  4sq  16935  symgval  19301  nosupcbv  27614  nosupdm  27616  noinfcbv  27629  noinfdm  27631  addsval2  27870  addscut  27885  addsunif  27909  addsasslem1  27910  addsasslem2  27911  mulsval2lem  28013  mulsunif2  28073  precsexlemcbv  28108  isuhgr  28987  isushgr  28988  isupgr  29011  isumgr  29022  isuspgr  29079  isusgr  29080  isconngr  30118  isconngr1  30119  dispcmp  33849  eulerpart  34373  ballotlemfmpn  34486  bnj66  34850  bnj1234  35003  subfacp1lem6  35172  subfacp1  35173  dfon2lem3  35773  dfon2lem7  35777  cbvsbcvw2  36218  cbvixpvw2  36233  bj-gabeqis  36926  f1omptsn  37325  rdgssun  37366  ismblfin  37655  glbconxN  39372  sticksstones15  42149  eldioph3  42754  diophrex  42763  cbvcllem  43598  cbvrabv2w  45122  ssfiunibd  45307  aiotajust  47085