Theorem cbvabv 2809

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536  [wsb 2061   ∈ wcel 2105  {cab 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726

This theorem is referenced by:  cbvrabv  3443  cbvsbcvw  3825  difjust  3964  unjust  3966  injust  3968  uniiunlem  4096  dfif3  4544  pwjust  4605  snjust  4629  intab  4982  intabs  5354  iotajust  6514  cbviotavw  6523  frrlem1  8309  wfrlem1OLD  8346  fsetprcnex  8900  sbth  9131  sbthfi  9236  cardprc  10017  iunfictbso  10151  aceq3lem  10157  isf33lem  10403  axdc3  10491  axdclem  10556  axdc  10558  genpv  11036  ltexpri  11080  recexpr  11088  supsr  11149  hashf1lem2  14491  cvbtrcl  15027  mertens  15918  4sq  16997  symgval  19402  nosupcbv  27761  nosupdm  27763  noinfcbv  27776  noinfdm  27778  addsval2  28010  addscut  28025  addsunif  28049  addsasslem1  28050  addsasslem2  28051  mulsval2lem  28150  mulsunif2  28210  precsexlemcbv  28244  isuhgr  29091  isushgr  29092  isupgr  29115  isumgr  29126  isuspgr  29183  isusgr  29184  isconngr  30217  isconngr1  30218  dispcmp  33819  eulerpart  34363  ballotlemfmpn  34475  bnj66  34852  bnj1234  35005  subfacp1lem6  35169  subfacp1  35170  dfon2lem3  35766  dfon2lem7  35770  cbvsbcvw2  36212  cbvixpvw2  36227  bj-gabeqis  36920  f1omptsn  37319  rdgssun  37360  ismblfin  37647  glbconxN  39360  sticksstones15  42142  eldioph3  42753  diophrex  42762  cbvcllem  43598  cbvrabv2w  45067  ssfiunibd  45259  aiotajust  47033