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 2160 and ax-13 2371. (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 2106	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑥]𝜑)
2		cbvabv.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	2	sbievw 2101	. . . . 5 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓)
4	3	sbbii 2084	. . . 4 ⊢ ([𝑧 / 𝑦][𝑦 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
5	1, 4	bitr3i 280	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
6		df-clab 2715	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
7		df-clab 2715	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
8	5, 6, 7	3bitr4i 306	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
9	8	eqriv 2733	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1543  [wsb 2072   ∈ wcel 2112  {cab 2714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728

This theorem is referenced by:  cbvrabv  3392  cbvsbcvw  3718  difjust  3855  unjust  3857  injust  3859  uniiunlem  3985  dfif3  4439  pwjust  4500  snjust  4526  intab  4875  intabs  5220  iotajust  6315  cbviotavw  6324  frrlem1  8005  wfrlem1  8032  fsetprcnex  8521  sbth  8744  cardprc  9561  iunfictbso  9693  aceq3lem  9699  isf33lem  9945  axdc3  10033  axdclem  10098  axdc  10100  genpv  10578  ltexpri  10622  recexpr  10630  supsr  10691  hashf1lem2  13987  cvbtrcl  14520  mertens  15413  4sq  16480  symgval  18715  isuhgr  27105  isushgr  27106  isupgr  27129  isumgr  27140  isuspgr  27197  isusgr  27198  isconngr  28226  isconngr1  28227  dispcmp  31477  eulerpart  32015  ballotlemfmpn  32127  bnj66  32507  bnj1234  32660  subfacp1lem6  32814  subfacp1  32815  dfon2lem3  33431  dfon2lem7  33435  nosupcbv  33591  nosupdm  33593  noinfcbv  33606  noinfdm  33608  bj-gabeqis  34812  f1omptsn  35194  rdgssun  35235  ismblfin  35504  glbconxN  37078  sticksstones15  39786  eldioph3  40232  diophrex  40241  cbvcllem  40834  ssfiunibd  42462  aiotajust  44191