Theorem cbvabv 2809

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  [wsb 2073   ∈ wcel 2119  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731

This theorem is referenced by:  cbvrabv  3401  cbvsbcvw  3757  difjust  3885  unjust  3887  injust  3889  uniiunlem  4018  dfif3  4469  pwjust  4530  snjust  4554  intab  4908  intabs  5277  iotajust  6440  cbviotavw  6449  frrlem1  8226  fsetprcnex  8799  sbth  9025  sbthfi  9123  cardprc  9895  iunfictbso  10027  aceq3lem  10033  isf33lem  10279  axdc3  10367  axdclem  10432  axdc  10434  genpv  10913  ltexpri  10957  recexpr  10965  supsr  11026  hashf1lem2  14409  cvbtrcl  14945  mertens  15842  4sq  16926  symgval  19337  nosupcbv  27684  nosupdm  27686  noinfcbv  27699  noinfdm  27701  addsval2  27973  addcuts  27988  addsunif  28012  addsasslem1  28013  addsasslem2  28014  mulsval2lem  28120  mulsunif2  28180  precsexlemcbv  28216  isuhgr  29147  isushgr  29148  isupgr  29171  isumgr  29182  isuspgr  29239  isusgr  29240  isconngr  30277  isconngr1  30278  dispcmp  34043  eulerpart  34566  ballotlemfmpn  34679  bnj66  35042  bnj1234  35195  setinds2regs  35312  tz9.1regs  35315  subfacp1lem6  35413  subfacp1  35414  dfon2lem3  36011  dfon2lem7  36015  cbvsbcvw2  36458  cbvixpvw2  36473  bj-gabeqis  37291  f1omptsn  37699  rdgssun  37740  ismblfin  38028  glbconxN  39870  sticksstones15  42646  eldioph3  43215  diophrex  43224  cbvcllem  44053  cbvrabv2w  45575  ssfiunibd  45757  aiotajust  47547