Theorem cbvabv 2905

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2906 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2094 and ax-13 2302. (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 2045	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
2		cbvabv.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbievw 2042	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	sbbii 2028	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
5	1, 4	bitr3i 269	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
6		df-clab 2754	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
7		df-clab 2754	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
8	5, 6, 7	3bitr4i 295	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
9	8	eqriv 2770	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1508  [wsb 2016   ∈ wcel 2051  {cab 2753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-9 2060  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-sb 2017  df-clab 2754  df-cleq 2766

This theorem is referenced by:  cbvrabv  3407  difjust  3826  unjust  3828  injust  3830  uniiunlem  3946  dfif3  4359  pwjust  4418  snjust  4435  intab  4776  intabs  5098  iotajust  6149  wfrlem1  7756  sbth  8432  cardprc  9202  iunfictbso  9333  aceq3lem  9339  isf33lem  9585  axdc3  9673  axdclem  9738  axdc  9740  genpv  10218  ltexpri  10262  recexpr  10270  supsr  10331  hashf1lem2  13626  cvbtrcl  14212  mertens  15101  4sq  16155  isuhgr  26564  isushgr  26565  isupgr  26588  isumgr  26599  isuspgr  26656  isusgr  26657  isconngr  27734  isconngr1  27735  isfrgr  27808  dispcmp  30800  eulerpart  31318  ballotlemfmpn  31431  bnj66  31812  bnj1234  31963  subfacp1lem6  32050  subfacp1  32051  dfon2lem3  32583  dfon2lem7  32587  frrlem1  32677  nosupdm  32758  f1omptsn  34093  rdgssun  34134  ismblfin  34407  glbconxN  35992  eldioph3  38792  diophrex  38802  cbvcllem  39365  ssfiunibd  41035  aiotajust  42720