Theorem cbvabv 2815

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  [wsb 2064   ∈ wcel 2108  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732

This theorem is referenced by:  cbvrabv  3454  cbvsbcvw  3839  difjust  3978  unjust  3980  injust  3982  uniiunlem  4110  dfif3  4562  pwjust  4623  snjust  4647  intab  5002  intabs  5367  iotajust  6524  cbviotavw  6533  frrlem1  8327  wfrlem1OLD  8364  fsetprcnex  8920  sbth  9159  sbthfi  9265  cardprc  10049  iunfictbso  10183  aceq3lem  10189  isf33lem  10435  axdc3  10523  axdclem  10588  axdc  10590  genpv  11068  ltexpri  11112  recexpr  11120  supsr  11181  hashf1lem2  14505  cvbtrcl  15041  mertens  15934  4sq  17011  symgval  19412  nosupcbv  27765  nosupdm  27767  noinfcbv  27780  noinfdm  27782  addsval2  28014  addscut  28029  addsunif  28053  addsasslem1  28054  addsasslem2  28055  mulsval2lem  28154  mulsunif2  28214  precsexlemcbv  28248  isuhgr  29095  isushgr  29096  isupgr  29119  isumgr  29130  isuspgr  29187  isusgr  29188  isconngr  30221  isconngr1  30222  dispcmp  33805  eulerpart  34347  ballotlemfmpn  34459  bnj66  34836  bnj1234  34989  subfacp1lem6  35153  subfacp1  35154  dfon2lem3  35749  dfon2lem7  35753  cbvsbcvw2  36196  cbvixpvw2  36211  bj-gabeqis  36904  f1omptsn  37303  rdgssun  37344  ismblfin  37621  glbconxN  39335  sticksstones15  42118  eldioph3  42722  diophrex  42731  cbvcllem  43571  cbvrabv2w  45030  ssfiunibd  45224  aiotajust  46999