Theorem cbvabv 2877

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 1984	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1984	. 2 ⊢ Ⅎ𝑥𝜓
3		cbvabv.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
4	1, 2, 3	cbvab 2876	1 ⊢ {𝑥 ∣ 𝜑} = {𝑦 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1624  {cab 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745

This theorem is referenced by:  cdeqab1  3560  difjust  3709  unjust  3711  injust  3713  uniiunlem  3825  dfif3  4236  pwjust  4295  snjust  4312  intab  4651  intabs  4966  iotajust  6003  wfrlem1  7575  sbth  8237  cardprc  8988  iunfictbso  9119  aceq3lem  9125  isf33lem  9372  axdc3  9460  axdclem  9525  axdc  9527  genpv  10005  ltexpri  10049  recexpr  10057  supsr  10117  hashf1lem2  13424  cvbtrcl  13924  mertens  14809  4sq  15862  isuhgr  26146  isushgr  26147  isupgr  26170  isumgr  26181  isuspgr  26238  isusgr  26239  isconngr  27333  isconngr1  27334  isfrgr  27404  dispcmp  30227  eulerpart  30745  ballotlemfmpn  30857  bnj66  31229  bnj1234  31380  subfacp1lem6  31466  subfacp1  31467  dfon2lem3  31987  dfon2lem7  31991  frrlem1  32078  nosupdm  32148  f1omptsn  33487  ismblfin  33755  glbconxN  35159  eldioph3  37823  diophrex  37833  cbvcllem  38409  ssfiunibd  40014