Theorem cbvabv 2812

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2815 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2156 and ax-13 2372. (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 2102	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
2		cbvabv.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbievw 2097	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	sbbii 2080	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
5	1, 4	bitr3i 276	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
6		df-clab 2716	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
7		df-clab 2716	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
8	5, 6, 7	3bitr4i 302	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
9	8	eqriv 2735	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsb 2068   ∈ wcel 2108  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730

This theorem is referenced by:  cbvrabv  3416  cbvsbcvw  3746  difjust  3885  unjust  3887  injust  3889  uniiunlem  4015  dfif3  4470  pwjust  4531  snjust  4557  intab  4906  intabs  5261  iotajust  6375  cbviotavw  6384  frrlem1  8073  wfrlem1OLD  8110  fsetprcnex  8608  sbth  8833  sbthfi  8942  cardprc  9669  iunfictbso  9801  aceq3lem  9807  isf33lem  10053  axdc3  10141  axdclem  10206  axdc  10208  genpv  10686  ltexpri  10730  recexpr  10738  supsr  10799  hashf1lem2  14098  cvbtrcl  14631  mertens  15526  4sq  16593  symgval  18891  isuhgr  27333  isushgr  27334  isupgr  27357  isumgr  27368  isuspgr  27425  isusgr  27426  isconngr  28454  isconngr1  28455  dispcmp  31711  eulerpart  32249  ballotlemfmpn  32361  bnj66  32740  bnj1234  32893  subfacp1lem6  33047  subfacp1  33048  dfon2lem3  33667  dfon2lem7  33671  nosupcbv  33832  nosupdm  33834  noinfcbv  33847  noinfdm  33849  bj-gabeqis  35053  f1omptsn  35435  rdgssun  35476  ismblfin  35745  glbconxN  37319  sticksstones15  40045  eldioph3  40504  diophrex  40513  cbvcllem  41106  ssfiunibd  42738  aiotajust  44463