Theorem cbvabv 2891

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2893 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2161 and ax-13 2390. (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 2108	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
2		cbvabv.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbievw 2103	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	sbbii 2081	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
5	1, 4	bitr3i 279	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
6		df-clab 2802	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
7		df-clab 2802	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
8	5, 6, 7	3bitr4i 305	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
9	8	eqriv 2820	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  [wsb 2069   ∈ wcel 2114  {cab 2801

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816

This theorem is referenced by:  cbvrabv  3493  difjust  3940  unjust  3942  injust  3944  uniiunlem  4063  dfif3  4483  pwjust  4542  snjust  4568  intab  4908  intabs  5247  iotajust  6315  wfrlem1  7956  sbth  8639  cardprc  9411  iunfictbso  9542  aceq3lem  9548  isf33lem  9790  axdc3  9878  axdclem  9943  axdc  9945  genpv  10423  ltexpri  10467  recexpr  10475  supsr  10536  hashf1lem2  13817  cvbtrcl  14354  mertens  15244  4sq  16302  symgval  18499  isuhgr  26847  isushgr  26848  isupgr  26871  isumgr  26882  isuspgr  26939  isusgr  26940  isconngr  27970  isconngr1  27971  dispcmp  31125  eulerpart  31642  ballotlemfmpn  31754  bnj66  32134  bnj1234  32287  subfacp1lem6  32434  subfacp1  32435  dfon2lem3  33032  dfon2lem7  33036  frrlem1  33125  nosupdm  33206  f1omptsn  34620  rdgssun  34661  ismblfin  34935  glbconxN  36516  eldioph3  39370  diophrex  39379  cbvcllem  39976  ssfiunibd  41583  aiotajust  43291