Theorem cbvabv 2807

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068   ∈ wcel 2114  {cab 2715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729

This theorem is referenced by:  cbvrabv  3411  cbvsbcvw  3776  difjust  3905  unjust  3907  injust  3909  uniiunlem  4041  dfif3  4496  pwjust  4557  snjust  4581  intab  4935  intabs  5296  iotajust  6455  cbviotavw  6464  frrlem1  8238  fsetprcnex  8811  sbth  9037  sbthfi  9135  cardprc  9904  iunfictbso  10036  aceq3lem  10042  isf33lem  10288  axdc3  10376  axdclem  10441  axdc  10443  genpv  10922  ltexpri  10966  recexpr  10974  supsr  11035  hashf1lem2  14391  cvbtrcl  14927  mertens  15821  4sq  16904  symgval  19312  nosupcbv  27682  nosupdm  27684  noinfcbv  27697  noinfdm  27699  addsval2  27971  addcuts  27986  addsunif  28010  addsasslem1  28011  addsasslem2  28012  mulsval2lem  28118  mulsunif2  28178  precsexlemcbv  28214  isuhgr  29145  isushgr  29146  isupgr  29169  isumgr  29180  isuspgr  29237  isusgr  29238  isconngr  30276  isconngr1  30277  dispcmp  34037  eulerpart  34560  ballotlemfmpn  34673  bnj66  35036  bnj1234  35189  setinds2regs  35309  tz9.1regs  35312  subfacp1lem6  35401  subfacp1  35402  dfon2lem3  35999  dfon2lem7  36003  cbvsbcvw2  36446  cbvixpvw2  36461  bj-gabeqis  37186  f1omptsn  37592  rdgssun  37633  ismblfin  37912  glbconxN  39754  sticksstones15  42531  eldioph3  43123  diophrex  43132  cbvcllem  43965  cbvrabv2w  45487  ssfiunibd  45671  aiotajust  47444