Theorem cbvabv 2839

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  [wsb 2097   ∈ wcel 2149  {cab 2747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761

This theorem is referenced by:  cbvrabv  3433  cbvsbcvw  3787  difjust  3915  unjust  3917  injust  3919  uniiunlem  4049  dfif3  4507  pwjust  4568  snjust  4593  intab  4947  intabs  5320  iotajust  6492  cbviotavw  6501  frrlem1  8283  fsetprcnex  8859  sbth  9085  sbthfi  9183  cardprc  9966  iunfictbso  10098  aceq3lem  10104  isf33lem  10350  axdc3  10438  axdclem  10503  axdc  10505  genpv  10984  ltexpri  11028  recexpr  11036  supsr  11097  hashf1lem2  14493  cvbtrcl  15029  mertens  15940  4sq  17024  symgval  19441  nosupcbv  27832  nosupdm  27834  noinfcbv  27847  noinfdm  27849  addsval2  28122  addcuts  28137  addsunif  28161  addsasslem1  28162  addsasslem2  28163  mulsval2lem  28269  mulsunif2  28329  precsexlemcbv  28365  isuhgr  29351  isushgr  29352  isupgr  29375  isumgr  29386  isuspgr  29443  isusgr  29444  isconngr  30481  isconngr1  30482  dispcmp  34194  eulerpart  34717  ballotlemfmpn  34830  bnj66  35193  bnj1234  35346  setinds2regs  35477  tz9.1regs  35480  subfacp1lem6  35610  subfacp1  35611  dfon2lem3  36208  dfon2lem7  36212  cbvsbcvw2  36665  cbvixpvw2  36680  bj-gabeqis  37496  f1omptsn  37905  rdgssun  37946  ismblfin  38234  glbconxN  40076  sticksstones15  42852  eldioph3  43423  diophrex  43432  cbvcllem  44261  cbvrabv2w  45772  ssfiunibd  45954  aiotajust  47744