Theorem cbvabv 2834

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2101   ∈ wcel 2147  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755

This theorem is used by:  cbvrabv  3426  cbvsbcvw  3776  uniiunlem  4015  difjust  4049  injust  4093  unjust  4153  dfif3  4500  pwjust  4561  snjust  4587  intab  4943  intabs  5317  iotajust  6519  cbviotavw  6528  frrlem1  8342  fsetprcnex  8922  sbth  9154  sbthfi  9252  cardprc  10098  iunfictbso  10232  aceq3lem  10238  isf33lem  10483  axdc3  10571  axdclem  10636  axdc  10638  genpv  11123  ltexpri  11167  recexpr  11175  supsr  11236  hashf1lem2  14642  cvbtrcl  15188  mertens  16099  4sq  17186  symgval  19636  nosupcbv  28116  nosupdm  28118  noinfcbv  28131  noinfdm  28133  addsval2  28406  addcuts  28421  addsunif  28445  addsasslem1  28446  addsasslem2  28447  mulsval2lem  28553  mulsunif2  28613  precsexlemcbv  28649  isuhgr  29695  isushgr  29696  isupgr  29719  isumgr  29730  isuspgr  29790  isusgr  29791  isconngr  30847  isconngr1  30848  dispcmp  34602  eulerpart  35125  ballotlemfmpn  35238  bnj66  35601  bnj1234  35754  setinds2regs  35940  tz9.1regs  35943  subfacp1lem6  36158  subfacp1  36159  dfon2lem3  36762  dfon2lem7  36766  cbvsbcvw2  37234  cbvixpvw2  37249  bj-gabeqis  38066  f1omptsn  38528  rdgssun  38569  ismblfin  38847  glbconxN  40701  sticksstones15  43477  eldioph3  44043  diophrex  44052  cbvcllem  44870  cbvrabv2w  46416  ssfiunibd  46598  aiotajust  48427