Theorem cbvabv 2806

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

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

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 2708

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

This theorem is referenced by:  cbvrabv  3409  cbvsbcvw  3774  difjust  3903  unjust  3905  injust  3907  uniiunlem  4039  dfif3  4494  pwjust  4555  snjust  4579  intab  4933  intabs  5294  iotajust  6447  cbviotavw  6456  frrlem1  8228  fsetprcnex  8799  sbth  9025  sbthfi  9123  cardprc  9892  iunfictbso  10024  aceq3lem  10030  isf33lem  10276  axdc3  10364  axdclem  10429  axdc  10431  genpv  10910  ltexpri  10954  recexpr  10962  supsr  11023  hashf1lem2  14379  cvbtrcl  14915  mertens  15809  4sq  16892  symgval  19300  nosupcbv  27670  nosupdm  27672  noinfcbv  27685  noinfdm  27687  addsval2  27959  addcuts  27974  addsunif  27998  addsasslem1  27999  addsasslem2  28000  mulsval2lem  28106  mulsunif2  28166  precsexlemcbv  28202  isuhgr  29133  isushgr  29134  isupgr  29157  isumgr  29168  isuspgr  29225  isusgr  29226  isconngr  30264  isconngr1  30265  dispcmp  34016  eulerpart  34539  ballotlemfmpn  34652  bnj66  35016  bnj1234  35169  setinds2regs  35287  tz9.1regs  35290  subfacp1lem6  35379  subfacp1  35380  dfon2lem3  35977  dfon2lem7  35981  cbvsbcvw2  36424  cbvixpvw2  36439  bj-gabeqis  37139  f1omptsn  37542  rdgssun  37583  ismblfin  37862  glbconxN  39648  sticksstones15  42425  eldioph3  43018  diophrex  43027  cbvcllem  43860  cbvrabv2w  45382  ssfiunibd  45567  aiotajust  47340