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  3413  cbvsbcvw  3784  difjust  3913  unjust  3915  injust  3917  uniiunlem  4046  dfif3  4499  pwjust  4560  snjust  4584  intab  4938  intabs  5299  iotajust  6451  cbviotavw  6460  frrlem1  8242  fsetprcnex  8812  sbth  9038  sbthfi  9140  cardprc  9909  iunfictbso  10043  aceq3lem  10049  isf33lem  10295  axdc3  10383  axdclem  10448  axdc  10450  genpv  10928  ltexpri  10972  recexpr  10980  supsr  11041  hashf1lem2  14397  cvbtrcl  14934  mertens  15828  4sq  16911  symgval  19285  nosupcbv  27647  nosupdm  27649  noinfcbv  27662  noinfdm  27664  addsval2  27910  addscut  27925  addsunif  27949  addsasslem1  27950  addsasslem2  27951  mulsval2lem  28053  mulsunif2  28113  precsexlemcbv  28148  isuhgr  29040  isushgr  29041  isupgr  29064  isumgr  29075  isuspgr  29132  isusgr  29133  isconngr  30168  isconngr1  30169  dispcmp  33842  eulerpart  34366  ballotlemfmpn  34479  bnj66  34843  bnj1234  34996  subfacp1lem6  35165  subfacp1  35166  dfon2lem3  35766  dfon2lem7  35770  cbvsbcvw2  36211  cbvixpvw2  36226  bj-gabeqis  36919  f1omptsn  37318  rdgssun  37359  ismblfin  37648  glbconxN  39365  sticksstones15  42142  eldioph3  42747  diophrex  42756  cbvcllem  43591  cbvrabv2w  45115  ssfiunibd  45300  aiotajust  47078