Theorem cbvabv 2805

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2064   ∈ wcel 2108  {cab 2713

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727

This theorem is referenced by:  cbvrabv  3426  cbvsbcvw  3799  difjust  3928  unjust  3930  injust  3932  uniiunlem  4062  dfif3  4515  pwjust  4576  snjust  4600  intab  4954  intabs  5319  iotajust  6483  cbviotavw  6492  frrlem1  8285  wfrlem1OLD  8322  fsetprcnex  8876  sbth  9107  sbthfi  9213  cardprc  9994  iunfictbso  10128  aceq3lem  10134  isf33lem  10380  axdc3  10468  axdclem  10533  axdc  10535  genpv  11013  ltexpri  11057  recexpr  11065  supsr  11126  hashf1lem2  14474  cvbtrcl  15011  mertens  15902  4sq  16984  symgval  19352  nosupcbv  27666  nosupdm  27668  noinfcbv  27681  noinfdm  27683  addsval2  27922  addscut  27937  addsunif  27961  addsasslem1  27962  addsasslem2  27963  mulsval2lem  28065  mulsunif2  28125  precsexlemcbv  28160  isuhgr  29039  isushgr  29040  isupgr  29063  isumgr  29074  isuspgr  29131  isusgr  29132  isconngr  30170  isconngr1  30171  dispcmp  33890  eulerpart  34414  ballotlemfmpn  34527  bnj66  34891  bnj1234  35044  subfacp1lem6  35207  subfacp1  35208  dfon2lem3  35803  dfon2lem7  35807  cbvsbcvw2  36248  cbvixpvw2  36263  bj-gabeqis  36956  f1omptsn  37355  rdgssun  37396  ismblfin  37685  glbconxN  39397  sticksstones15  42174  eldioph3  42789  diophrex  42798  cbvcllem  43633  cbvrabv2w  45152  ssfiunibd  45338  aiotajust  47113