Theorem cbvabv 2806

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728

This theorem is referenced by:  cbvrabv  3399  cbvsbcvw  3762  difjust  3891  unjust  3893  injust  3895  uniiunlem  4027  dfif3  4481  pwjust  4542  snjust  4566  intab  4920  intabs  5290  iotajust  6453  cbviotavw  6462  frrlem1  8236  fsetprcnex  8809  sbth  9035  sbthfi  9133  cardprc  9904  iunfictbso  10036  aceq3lem  10042  isf33lem  10288  axdc3  10376  axdclem  10441  axdc  10443  genpv  10922  ltexpri  10966  recexpr  10974  supsr  11035  hashf1lem2  14418  cvbtrcl  14954  mertens  15851  4sq  16935  symgval  19346  nosupcbv  27666  nosupdm  27668  noinfcbv  27681  noinfdm  27683  addsval2  27955  addcuts  27970  addsunif  27994  addsasslem1  27995  addsasslem2  27996  mulsval2lem  28102  mulsunif2  28162  precsexlemcbv  28198  isuhgr  29129  isushgr  29130  isupgr  29153  isumgr  29164  isuspgr  29221  isusgr  29222  isconngr  30259  isconngr1  30260  dispcmp  34003  eulerpart  34526  ballotlemfmpn  34639  bnj66  35002  bnj1234  35155  setinds2regs  35275  tz9.1regs  35278  subfacp1lem6  35367  subfacp1  35368  dfon2lem3  35965  dfon2lem7  35969  cbvsbcvw2  36412  cbvixpvw2  36427  bj-gabeqis  37245  f1omptsn  37653  rdgssun  37694  ismblfin  37982  glbconxN  39824  sticksstones15  42600  eldioph3  43198  diophrex  43207  cbvcllem  44036  cbvrabv2w  45558  ssfiunibd  45742  aiotajust  47532