Theorem cbvabv 2803

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2065   ∈ wcel 2104  {cab 2707

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722

This theorem is referenced by:  cbvrabv  3440  cbvsbcvw  3813  difjust  3951  unjust  3953  injust  3955  uniiunlem  4085  dfif3  4543  pwjust  4604  snjust  4628  intab  4983  intabs  5343  iotajust  6495  cbviotavw  6504  frrlem1  8275  wfrlem1OLD  8312  fsetprcnex  8860  sbth  9097  sbthfi  9206  cardprc  9979  iunfictbso  10113  aceq3lem  10119  isf33lem  10365  axdc3  10453  axdclem  10518  axdc  10520  genpv  10998  ltexpri  11042  recexpr  11050  supsr  11111  hashf1lem2  14423  cvbtrcl  14945  mertens  15838  4sq  16903  symgval  19279  nosupcbv  27439  nosupdm  27441  noinfcbv  27454  noinfdm  27456  addsval2  27683  addscut  27698  addsunif  27722  addsasslem1  27723  addsasslem2  27724  mulsval2lem  27803  precsexlemcbv  27889  isuhgr  28585  isushgr  28586  isupgr  28609  isumgr  28620  isuspgr  28677  isusgr  28678  isconngr  29707  isconngr1  29708  dispcmp  33135  eulerpart  33677  ballotlemfmpn  33789  bnj66  34167  bnj1234  34320  subfacp1lem6  34472  subfacp1  34473  dfon2lem3  35059  dfon2lem7  35063  bj-gabeqis  36123  f1omptsn  36523  rdgssun  36564  ismblfin  36834  glbconxN  38554  sticksstones15  41285  eldioph3  41808  diophrex  41817  cbvcllem  42664  ssfiunibd  44319  aiotajust  46092