Theorem cbvabv 2832

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1560  [wsb 2090   ∈ wcel 2142  {cab 2740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754

This theorem is referenced by:  cbvrabv  3424  cbvsbcvw  3778  difjust  3906  unjust  3908  injust  3910  uniiunlem  4040  dfif3  4495  pwjust  4556  snjust  4581  intab  4936  intabs  5305  iotajust  6476  cbviotavw  6485  frrlem1  8267  fsetprcnex  8843  sbth  9069  sbthfi  9167  cardprc  9938  iunfictbso  10070  aceq3lem  10076  isf33lem  10323  axdc3  10411  axdclem  10476  axdc  10478  genpv  10957  ltexpri  11001  recexpr  11009  supsr  11070  hashf1lem2  14469  cvbtrcl  15005  mertens  15916  4sq  17000  symgval  19411  nosupcbv  27766  nosupdm  27768  noinfcbv  27781  noinfdm  27783  addsval2  28056  addcuts  28071  addsunif  28095  addsasslem1  28096  addsasslem2  28097  mulsval2lem  28203  mulsunif2  28263  precsexlemcbv  28299  isuhgr  29261  isushgr  29262  isupgr  29285  isumgr  29296  isuspgr  29353  isusgr  29354  isconngr  30391  isconngr1  30392  dispcmp  34156  eulerpart  34679  ballotlemfmpn  34792  bnj66  35155  bnj1234  35308  setinds2regs  35427  tz9.1regs  35430  subfacp1lem6  35535  subfacp1  35536  dfon2lem3  36133  dfon2lem7  36137  cbvsbcvw2  36590  cbvixpvw2  36605  bj-gabeqis  37423  f1omptsn  37831  rdgssun  37872  ismblfin  38160  glbconxN  40002  sticksstones15  42778  eldioph3  43347  diophrex  43356  cbvcllem  44185  cbvrabv2w  45706  ssfiunibd  45888  aiotajust  47678