Theorem cbvabv 2831

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099   ∈ wcel 2145  {cab 2739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753

This theorem is used by:  cbvrabv  3423  cbvsbcvw  3773  difjust  3901  unjust  3903  injust  3905  uniiunlem  4035  dfif3  4497  pwjust  4558  snjust  4583  intab  4938  intabs  5310  iotajust  6493  cbviotavw  6502  frrlem1  8304  fsetprcnex  8884  sbth  9116  sbthfi  9214  cardprc  10061  iunfictbso  10193  aceq3lem  10199  isf33lem  10444  axdc3  10532  axdclem  10597  axdc  10599  genpv  11084  ltexpri  11128  recexpr  11136  supsr  11197  hashf1lem2  14601  cvbtrcl  15145  mertens  16055  4sq  17142  symgval  19585  nosupcbv  28059  nosupdm  28061  noinfcbv  28074  noinfdm  28076  addsval2  28349  addcuts  28364  addsunif  28388  addsasslem1  28389  addsasslem2  28390  mulsval2lem  28496  mulsunif2  28556  precsexlemcbv  28592  isuhgr  29638  isushgr  29639  isupgr  29662  isumgr  29673  isuspgr  29733  isusgr  29734  isconngr  30790  isconngr1  30791  dispcmp  34491  eulerpart  35014  ballotlemfmpn  35127  bnj66  35490  bnj1234  35643  setinds2regs  35799  tz9.1regs  35802  subfacp1lem6  35950  subfacp1  35951  dfon2lem3  36547  dfon2lem7  36551  cbvsbcvw2  37019  cbvixpvw2  37034  bj-gabeqis  37851  f1omptsn  38260  rdgssun  38301  ismblfin  38579  glbconxN  40435  sticksstones15  43211  eldioph3  43776  diophrex  43785  cbvcllem  44608  cbvrabv2w  46142  ssfiunibd  46324  aiotajust  48153