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 2147 and ax-13 2366. (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 2354	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
3		df-clab 2704	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
4		df-clab 2704	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
5	2, 3, 4	3bitr4i 302	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
6	5	eqriv 2723	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  [wsb 2060   ∈ wcel 2099  {cab 2703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718

This theorem is referenced by:  cbvrabv  3430  cbvsbcvw  3811  difjust  3949  unjust  3951  injust  3953  uniiunlem  4083  dfif3  4547  pwjust  4608  snjust  4632  intab  4986  intabs  5349  iotajust  6505  cbviotavw  6514  frrlem1  8301  wfrlem1OLD  8338  fsetprcnex  8891  sbth  9131  sbthfi  9236  cardprc  10023  iunfictbso  10157  aceq3lem  10163  isf33lem  10409  axdc3  10497  axdclem  10562  axdc  10564  genpv  11042  ltexpri  11086  recexpr  11094  supsr  11155  hashf1lem2  14475  cvbtrcl  14997  mertens  15890  4sq  16966  symgval  19366  nosupcbv  27732  nosupdm  27734  noinfcbv  27747  noinfdm  27749  addsval2  27977  addscut  27992  addsunif  28016  addsasslem1  28017  addsasslem2  28018  mulsval2lem  28111  mulsunif2  28171  precsexlemcbv  28205  isuhgr  28996  isushgr  28997  isupgr  29020  isumgr  29031  isuspgr  29088  isusgr  29089  isconngr  30122  isconngr1  30123  dispcmp  33674  eulerpart  34216  ballotlemfmpn  34328  bnj66  34705  bnj1234  34858  subfacp1lem6  35013  subfacp1  35014  dfon2lem3  35609  dfon2lem7  35613  bj-gabeqis  36644  f1omptsn  37044  rdgssun  37085  ismblfin  37362  glbconxN  39077  sticksstones15  41859  eldioph3  42423  diophrex  42432  cbvcllem  43276  ssfiunibd  44924  aiotajust  46697