Theorem cbvabv 2833

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2835 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2196 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 2138	. . 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 1569  [wsb 2100   ∈ wcel 2146  {cab 2741

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

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

This theorem is used by:  cbvrabv  3425  cbvsbcvw  3775  uniiunlem  4014  difjust  4048  injust  4092  unjust  4152  dfif3  4499  pwjust  4560  snjust  4586  intab  4940  intabs  5313  iotajust  6499  cbviotavw  6508  frrlem1  8315  fsetprcnex  8895  sbth  9127  sbthfi  9225  cardprc  10071  iunfictbso  10203  aceq3lem  10209  isf33lem  10454  axdc3  10542  axdclem  10607  axdc  10609  genpv  11094  ltexpri  11138  recexpr  11146  supsr  11207  hashf1lem2  14611  cvbtrcl  15157  mertens  16067  4sq  17154  symgval  19597  nosupcbv  28071  nosupdm  28073  noinfcbv  28086  noinfdm  28088  addsval2  28361  addcuts  28376  addsunif  28400  addsasslem1  28401  addsasslem2  28402  mulsval2lem  28508  mulsunif2  28568  precsexlemcbv  28604  isuhgr  29650  isushgr  29651  isupgr  29674  isumgr  29685  isuspgr  29745  isusgr  29746  isconngr  30802  isconngr1  30803  dispcmp  34544  eulerpart  35067  ballotlemfmpn  35180  bnj66  35543  bnj1234  35696  setinds2regs  35870  tz9.1regs  35873  subfacp1lem6  36071  subfacp1  36072  dfon2lem3  36674  dfon2lem7  36678  cbvsbcvw2  37146  cbvixpvw2  37161  bj-gabeqis  37978  f1omptsn  38400  rdgssun  38441  ismblfin  38719  glbconxN  40575  sticksstones15  43351  eldioph3  43917  diophrex  43926  cbvcllem  44749  cbvrabv2w  46282  ssfiunibd  46464  aiotajust  48293