Theorem cbvabv 2835

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  cbvrabv  3428  cbvsbcvw  3780  difjust  3908  unjust  3910  injust  3912  uniiunlem  4042  dfif3  4504  pwjust  4565  snjust  4590  intab  4945  intabs  5321  iotajust  6495  cbviotavw  6504  frrlem1  8289  fsetprcnex  8865  sbth  9092  sbthfi  9190  cardprc  9982  iunfictbso  10114  aceq3lem  10120  isf33lem  10365  axdc3  10453  axdclem  10518  axdc  10520  genpv  11001  ltexpri  11045  recexpr  11053  supsr  11114  hashf1lem2  14513  cvbtrcl  15055  mertens  15965  4sq  17048  symgval  19487  nosupcbv  27919  nosupdm  27921  noinfcbv  27934  noinfdm  27936  addsval2  28209  addcuts  28224  addsunif  28248  addsasslem1  28249  addsasslem2  28250  mulsval2lem  28356  mulsunif2  28416  precsexlemcbv  28452  isuhgr  29467  isushgr  29468  isupgr  29491  isumgr  29502  isuspgr  29562  isusgr  29563  isconngr  30613  isconngr1  30614  dispcmp  34315  eulerpart  34839  ballotlemfmpn  34952  bnj66  35315  bnj1234  35468  setinds2regs  35603  tz9.1regs  35606  subfacp1lem6  35716  subfacp1  35717  dfon2lem3  36314  dfon2lem7  36318  cbvsbcvw2  36801  cbvixpvw2  36816  bj-gabeqis  37633  f1omptsn  38042  rdgssun  38083  ismblfin  38371  glbconxN  40212  sticksstones15  42988  eldioph3  43557  diophrex  43566  cbvcllem  44395  cbvrabv2w  45906  ssfiunibd  46088  aiotajust  47881