Theorem cbvabv 2801

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2067   ∈ wcel 2111  {cab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723

This theorem is referenced by:  cbvrabv  3405  cbvsbcvw  3770  difjust  3899  unjust  3901  injust  3903  uniiunlem  4034  dfif3  4487  pwjust  4548  snjust  4572  intab  4926  intabs  5285  iotajust  6436  cbviotavw  6445  frrlem1  8216  fsetprcnex  8786  sbth  9010  sbthfi  9108  cardprc  9873  iunfictbso  10005  aceq3lem  10011  isf33lem  10257  axdc3  10345  axdclem  10410  axdc  10412  genpv  10890  ltexpri  10934  recexpr  10942  supsr  11003  hashf1lem2  14363  cvbtrcl  14899  mertens  15793  4sq  16876  symgval  19283  nosupcbv  27641  nosupdm  27643  noinfcbv  27656  noinfdm  27658  addsval2  27906  addscut  27921  addsunif  27945  addsasslem1  27946  addsasslem2  27947  mulsval2lem  28049  mulsunif2  28109  precsexlemcbv  28144  isuhgr  29038  isushgr  29039  isupgr  29062  isumgr  29073  isuspgr  29130  isusgr  29131  isconngr  30169  isconngr1  30170  dispcmp  33872  eulerpart  34395  ballotlemfmpn  34508  bnj66  34872  bnj1234  35025  setinds2regs  35129  tz9.1regs  35130  subfacp1lem6  35229  subfacp1  35230  dfon2lem3  35827  dfon2lem7  35831  cbvsbcvw2  36274  cbvixpvw2  36289  bj-gabeqis  36982  f1omptsn  37381  rdgssun  37422  ismblfin  37711  glbconxN  39487  sticksstones15  42264  eldioph3  42869  diophrex  42878  cbvcllem  43712  cbvrabv2w  45235  ssfiunibd  45420  aiotajust  47194