Theorem cbvabv 2927

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)

Hypothesis

Ref	Expression
cbvabv.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
cbvabv	⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvabv

Step	Hyp	Ref	Expression
1		nfv 2005	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 2005	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvabv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvab 2926	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  {cab 2788

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795

This theorem is referenced by:  cdeqab1  3619  difjust  3765  unjust  3767  injust  3769  uniiunlem  3883  dfif3  4287  pwjust  4346  snjust  4363  intab  4692  intabs  5011  iotajust  6057  wfrlem1  7643  sbth  8313  cardprc  9083  iunfictbso  9214  aceq3lem  9220  isf33lem  9467  axdc3  9555  axdclem  9620  axdc  9622  genpv  10100  ltexpri  10144  recexpr  10152  supsr  10212  hashf1lem2  13451  cvbtrcl  13950  mertens  14833  4sq  15879  isuhgr  26163  isushgr  26164  isupgr  26187  isumgr  26198  isuspgr  26256  isusgr  26257  isconngr  27356  isconngr1  27357  isfrgr  27427  dispcmp  30245  eulerpart  30763  ballotlemfmpn  30875  bnj66  31247  bnj1234  31398  subfacp1lem6  31484  subfacp1  31485  dfon2lem3  32004  dfon2lem7  32008  frrlem1  32095  nosupdm  32165  f1omptsn  33495  ismblfin  33757  glbconxN  35152  eldioph3  37825  diophrex  37835  cbvcllem  38409  ssfiunibd  39998  aiotajust  41662