Theorem cbvabv 2800

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2802 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2158 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		cbvabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	cbvsbv 2101	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
3		df-clab 2709	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
4		df-clab 2709	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
5	2, 3, 4	3bitr4i 303	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
6	5	eqriv 2727	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722

This theorem is referenced by:  cbvrabv  3419  cbvsbcvw  3790  difjust  3919  unjust  3921  injust  3923  uniiunlem  4053  dfif3  4506  pwjust  4567  snjust  4591  intab  4945  intabs  5307  iotajust  6466  cbviotavw  6475  frrlem1  8268  fsetprcnex  8838  sbth  9067  sbthfi  9169  cardprc  9940  iunfictbso  10074  aceq3lem  10080  isf33lem  10326  axdc3  10414  axdclem  10479  axdc  10481  genpv  10959  ltexpri  11003  recexpr  11011  supsr  11072  hashf1lem2  14428  cvbtrcl  14965  mertens  15859  4sq  16942  symgval  19308  nosupcbv  27621  nosupdm  27623  noinfcbv  27636  noinfdm  27638  addsval2  27877  addscut  27892  addsunif  27916  addsasslem1  27917  addsasslem2  27918  mulsval2lem  28020  mulsunif2  28080  precsexlemcbv  28115  isuhgr  28994  isushgr  28995  isupgr  29018  isumgr  29029  isuspgr  29086  isusgr  29087  isconngr  30125  isconngr1  30126  dispcmp  33856  eulerpart  34380  ballotlemfmpn  34493  bnj66  34857  bnj1234  35010  subfacp1lem6  35179  subfacp1  35180  dfon2lem3  35780  dfon2lem7  35784  cbvsbcvw2  36225  cbvixpvw2  36240  bj-gabeqis  36933  f1omptsn  37332  rdgssun  37373  ismblfin  37662  glbconxN  39379  sticksstones15  42156  eldioph3  42761  diophrex  42770  cbvcllem  43605  cbvrabv2w  45129  ssfiunibd  45314  aiotajust  47089