Theorem cbvabv 2811

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730

This theorem is referenced by:  cbvrabv  3426  cbvsbcvw  3751  difjust  3889  unjust  3891  injust  3893  uniiunlem  4019  dfif3  4473  pwjust  4534  snjust  4560  intab  4909  intabs  5266  iotajust  6390  cbviotavw  6399  frrlem1  8102  wfrlem1OLD  8139  fsetprcnex  8650  sbth  8880  sbthfi  8985  cardprc  9738  iunfictbso  9870  aceq3lem  9876  isf33lem  10122  axdc3  10210  axdclem  10275  axdc  10277  genpv  10755  ltexpri  10799  recexpr  10807  supsr  10868  hashf1lem2  14170  cvbtrcl  14703  mertens  15598  4sq  16665  symgval  18976  isuhgr  27430  isushgr  27431  isupgr  27454  isumgr  27465  isuspgr  27522  isusgr  27523  isconngr  28553  isconngr1  28554  dispcmp  31809  eulerpart  32349  ballotlemfmpn  32461  bnj66  32840  bnj1234  32993  subfacp1lem6  33147  subfacp1  33148  dfon2lem3  33761  dfon2lem7  33765  nosupcbv  33905  nosupdm  33907  noinfcbv  33920  noinfdm  33922  bj-gabeqis  35126  f1omptsn  35508  rdgssun  35549  ismblfin  35818  glbconxN  37392  sticksstones15  40117  eldioph3  40588  diophrex  40597  cbvcllem  41217  ssfiunibd  42848  aiotajust  44576