Theorem cbvabv 2830

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099   ∈ wcel 2145  {cab 2738

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752

This theorem is used by:  cbvrabv  3422  cbvsbcvw  3773  difjust  3901  unjust  3903  injust  3905  uniiunlem  4035  dfif3  4497  pwjust  4558  snjust  4583  intab  4938  intabs  5313  iotajust  6488  cbviotavw  6497  frrlem1  8286  fsetprcnex  8866  sbth  9098  sbthfi  9196  cardprc  9988  iunfictbso  10120  aceq3lem  10126  isf33lem  10371  axdc3  10459  axdclem  10524  axdc  10526  genpv  11011  ltexpri  11055  recexpr  11063  supsr  11124  hashf1lem2  14524  cvbtrcl  15068  mertens  15978  4sq  17059  symgval  19501  nosupcbv  27941  nosupdm  27943  noinfcbv  27956  noinfdm  27958  addsval2  28231  addcuts  28246  addsunif  28270  addsasslem1  28271  addsasslem2  28272  mulsval2lem  28378  mulsunif2  28438  precsexlemcbv  28474  isuhgr  29520  isushgr  29521  isupgr  29544  isumgr  29555  isuspgr  29615  isusgr  29616  isconngr  30672  isconngr1  30673  dispcmp  34372  eulerpart  34896  ballotlemfmpn  35009  bnj66  35372  bnj1234  35525  setinds2regs  35660  tz9.1regs  35663  subfacp1lem6  35767  subfacp1  35768  dfon2lem3  36365  dfon2lem7  36369  cbvsbcvw2  36853  cbvixpvw2  36868  bj-gabeqis  37685  f1omptsn  38094  rdgssun  38135  ismblfin  38413  glbconxN  40254  sticksstones15  43030  eldioph3  43614  diophrex  43623  cbvcllem  44452  cbvrabv2w  45963  ssfiunibd  46145  aiotajust  47975