Theorem cbvabv 2812

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

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

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 2708

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

This theorem is referenced by:  cbvrabv  3447  cbvsbcvw  3822  difjust  3953  unjust  3955  injust  3957  uniiunlem  4087  dfif3  4540  pwjust  4601  snjust  4625  intab  4978  intabs  5349  iotajust  6513  cbviotavw  6522  frrlem1  8311  wfrlem1OLD  8348  fsetprcnex  8902  sbth  9133  sbthfi  9239  cardprc  10020  iunfictbso  10154  aceq3lem  10160  isf33lem  10406  axdc3  10494  axdclem  10559  axdc  10561  genpv  11039  ltexpri  11083  recexpr  11091  supsr  11152  hashf1lem2  14495  cvbtrcl  15031  mertens  15922  4sq  17002  symgval  19388  nosupcbv  27747  nosupdm  27749  noinfcbv  27762  noinfdm  27764  addsval2  27996  addscut  28011  addsunif  28035  addsasslem1  28036  addsasslem2  28037  mulsval2lem  28136  mulsunif2  28196  precsexlemcbv  28230  isuhgr  29077  isushgr  29078  isupgr  29101  isumgr  29112  isuspgr  29169  isusgr  29170  isconngr  30208  isconngr1  30209  dispcmp  33858  eulerpart  34384  ballotlemfmpn  34497  bnj66  34874  bnj1234  35027  subfacp1lem6  35190  subfacp1  35191  dfon2lem3  35786  dfon2lem7  35790  cbvsbcvw2  36231  cbvixpvw2  36246  bj-gabeqis  36939  f1omptsn  37338  rdgssun  37379  ismblfin  37668  glbconxN  39380  sticksstones15  42162  eldioph3  42777  diophrex  42786  cbvcllem  43622  cbvrabv2w  45133  ssfiunibd  45321  aiotajust  47096