Theorem cbvabv 2807

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729

This theorem is referenced by:  cbvrabv  3400  cbvsbcvw  3763  difjust  3892  unjust  3894  injust  3896  uniiunlem  4028  dfif3  4482  pwjust  4543  snjust  4567  intab  4921  intabs  5287  iotajust  6448  cbviotavw  6457  frrlem1  8230  fsetprcnex  8803  sbth  9029  sbthfi  9127  cardprc  9898  iunfictbso  10030  aceq3lem  10036  isf33lem  10282  axdc3  10370  axdclem  10435  axdc  10437  genpv  10916  ltexpri  10960  recexpr  10968  supsr  11029  hashf1lem2  14412  cvbtrcl  14948  mertens  15845  4sq  16929  symgval  19340  nosupcbv  27683  nosupdm  27685  noinfcbv  27698  noinfdm  27700  addsval2  27972  addcuts  27987  addsunif  28011  addsasslem1  28012  addsasslem2  28013  mulsval2lem  28119  mulsunif2  28179  precsexlemcbv  28215  isuhgr  29146  isushgr  29147  isupgr  29170  isumgr  29181  isuspgr  29238  isusgr  29239  isconngr  30277  isconngr1  30278  dispcmp  34022  eulerpart  34545  ballotlemfmpn  34658  bnj66  35021  bnj1234  35174  setinds2regs  35294  tz9.1regs  35297  subfacp1lem6  35386  subfacp1  35387  dfon2lem3  35984  dfon2lem7  35988  cbvsbcvw2  36431  cbvixpvw2  36446  bj-gabeqis  37264  f1omptsn  37670  rdgssun  37711  ismblfin  37999  glbconxN  39841  sticksstones15  42617  eldioph3  43215  diophrex  43224  cbvcllem  44057  cbvrabv2w  45579  ssfiunibd  45763  aiotajust  47547