Theorem cbvabv 2806

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1542  [wsb 2068   ∈ wcel 2107  {cab 2710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725

This theorem is referenced by:  cbvrabv  3443  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  8271  wfrlem1OLD  8308  fsetprcnex  8856  sbth  9093  sbthfi  9202  cardprc  9975  iunfictbso  10109  aceq3lem  10115  isf33lem  10361  axdc3  10449  axdclem  10514  axdc  10516  genpv  10994  ltexpri  11038  recexpr  11046  supsr  11107  hashf1lem2  14417  cvbtrcl  14939  mertens  15832  4sq  16897  symgval  19236  nosupcbv  27205  nosupdm  27207  noinfcbv  27220  noinfdm  27222  addsval2  27449  addscut  27464  addsunif  27488  addsasslem1  27489  addsasslem2  27490  mulsval2lem  27569  precsexlemcbv  27655  isuhgr  28351  isushgr  28352  isupgr  28375  isumgr  28386  isuspgr  28443  isusgr  28444  isconngr  29473  isconngr1  29474  dispcmp  32870  eulerpart  33412  ballotlemfmpn  33524  bnj66  33902  bnj1234  34055  subfacp1lem6  34207  subfacp1  34208  dfon2lem3  34788  dfon2lem7  34792  bj-gabeqis  35866  f1omptsn  36266  rdgssun  36307  ismblfin  36577  glbconxN  38297  sticksstones15  41025  eldioph3  41552  diophrex  41561  cbvcllem  42408  ssfiunibd  44067  aiotajust  45840