Theorem cbvabv 2833

Description: Rule used to change bound variables, using implicit substitution. Version of cbvab 2835 with disjoint variable conditions requiring fewer axioms. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2192 and ax-13 2404. (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 2135	. . 3 ⊢ ([𝑧 / 𝑥]𝜑 ↔ [𝑧 / 𝑦]𝜓)
3		df-clab 2742	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ [𝑧 / 𝑥]𝜑)
4		df-clab 2742	. . 3 ⊢ (𝑧 ∈ {𝑦 ∣ 𝜓} ↔ [𝑧 / 𝑦]𝜓)
5	2, 3, 4	3bitr4i 306	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ 𝜑} ↔ 𝑧 ∈ {𝑦 ∣ 𝜓})
6	5	eqriv 2760	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2096   ∈ wcel 2143  {cab 2741

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755

This theorem is referenced by:  cbvrabv  3426  cbvsbcvw  3778  difjust  3907  unjust  3909  injust  3911  uniiunlem  4041  dfif3  4502  pwjust  4563  snjust  4588  intab  4943  intabs  5319  iotajust  6491  cbviotavw  6500  frrlem1  8279  fsetprcnex  8855  sbth  9081  sbthfi  9179  cardprc  9962  iunfictbso  10094  aceq3lem  10100  isf33lem  10345  axdc3  10433  axdclem  10498  axdc  10500  genpv  10979  ltexpri  11023  recexpr  11031  supsr  11092  hashf1lem2  14489  cvbtrcl  15025  mertens  15936  4sq  17019  symgval  19436  nosupcbv  27866  nosupdm  27868  noinfcbv  27881  noinfdm  27883  addsval2  28156  addcuts  28171  addsunif  28195  addsasslem1  28196  addsasslem2  28197  mulsval2lem  28303  mulsunif2  28363  precsexlemcbv  28399  isuhgr  29410  isushgr  29411  isupgr  29434  isumgr  29445  isuspgr  29502  isusgr  29503  isconngr  30540  isconngr1  30541  dispcmp  34249  eulerpart  34772  ballotlemfmpn  34885  bnj66  35248  bnj1234  35401  setinds2regs  35544  tz9.1regs  35547  subfacp1lem6  35677  subfacp1  35678  dfon2lem3  36275  dfon2lem7  36279  cbvsbcvw2  36762  cbvixpvw2  36777  bj-gabeqis  37594  f1omptsn  38003  rdgssun  38044  ismblfin  38332  glbconxN  40172  sticksstones15  42948  eldioph3  43517  diophrex  43526  cbvcllem  44355  cbvrabv2w  45866  ssfiunibd  46048  aiotajust  47841