Theorem cbvabv 2804

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 2154 and ax-13 2370. (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		sbco2vv 2100	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
2		cbvabv.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbievw 2095	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	sbbii 2079	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
5	1, 4	bitr3i 276	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
6		df-clab 2709	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
7		df-clab 2709	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
8	5, 6, 7	3bitr4i 302	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
9	8	eqriv 2728	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  [wsb 2067   ∈ wcel 2106  {cab 2708

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723

This theorem is referenced by:  cbvrabv  3415  cbvsbcvw  3777  difjust  3915  unjust  3917  injust  3919  uniiunlem  4049  dfif3  4505  pwjust  4566  snjust  4590  intab  4944  intabs  5304  iotajust  6452  cbviotavw  6461  frrlem1  8222  wfrlem1OLD  8259  fsetprcnex  8807  sbth  9044  sbthfi  9153  cardprc  9925  iunfictbso  10059  aceq3lem  10065  isf33lem  10311  axdc3  10399  axdclem  10464  axdc  10466  genpv  10944  ltexpri  10988  recexpr  10996  supsr  11057  hashf1lem2  14367  cvbtrcl  14889  mertens  15782  4sq  16847  symgval  19164  nosupcbv  27087  nosupdm  27089  noinfcbv  27102  noinfdm  27104  addsval2  27318  addsasslem1  27354  addsasslem2  27355  isuhgr  28074  isushgr  28075  isupgr  28098  isumgr  28109  isuspgr  28166  isusgr  28167  isconngr  29196  isconngr1  29197  dispcmp  32529  eulerpart  33071  ballotlemfmpn  33183  bnj66  33561  bnj1234  33714  subfacp1lem6  33866  subfacp1  33867  dfon2lem3  34446  dfon2lem7  34450  bj-gabeqis  35481  f1omptsn  35881  rdgssun  35922  ismblfin  36192  glbconxN  37914  sticksstones15  40642  eldioph3  41147  diophrex  41156  cbvcllem  42003  ssfiunibd  43664  aiotajust  45436