Theorem cbvabv 2800

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsb 2066   ∈ wcel 2110  {cab 2708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722

This theorem is referenced by:  cbvrabv  3403  cbvsbcvw  3773  difjust  3902  unjust  3904  injust  3906  uniiunlem  4035  dfif3  4488  pwjust  4549  snjust  4573  intab  4926  intabs  5285  iotajust  6432  cbviotavw  6441  frrlem1  8211  fsetprcnex  8781  sbth  9005  sbthfi  9103  cardprc  9865  iunfictbso  9997  aceq3lem  10003  isf33lem  10249  axdc3  10337  axdclem  10402  axdc  10404  genpv  10882  ltexpri  10926  recexpr  10934  supsr  10995  hashf1lem2  14355  cvbtrcl  14891  mertens  15785  4sq  16868  symgval  19276  nosupcbv  27634  nosupdm  27636  noinfcbv  27649  noinfdm  27651  addsval2  27899  addscut  27914  addsunif  27938  addsasslem1  27939  addsasslem2  27940  mulsval2lem  28042  mulsunif2  28102  precsexlemcbv  28137  isuhgr  29031  isushgr  29032  isupgr  29055  isumgr  29066  isuspgr  29123  isusgr  29124  isconngr  30159  isconngr1  30160  dispcmp  33862  eulerpart  34385  ballotlemfmpn  34498  bnj66  34862  bnj1234  35015  setinds2regs  35101  tz9.1regs  35102  subfacp1lem6  35197  subfacp1  35198  dfon2lem3  35798  dfon2lem7  35802  cbvsbcvw2  36243  cbvixpvw2  36258  bj-gabeqis  36951  f1omptsn  37350  rdgssun  37391  ismblfin  37680  glbconxN  39396  sticksstones15  42173  eldioph3  42778  diophrex  42787  cbvcllem  43621  cbvrabv2w  45144  ssfiunibd  45329  aiotajust  47094