Theorem cbvabv 2734

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  {cab 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603

This theorem is referenced by:  cdeqab1  3394  difjust  3542  unjust  3544  injust  3546  uniiunlem  3653  dfif3  4050  pwjust  4109  snjust  4124  intab  4442  intabs  4752  iotajust  5767  wfrlem1  7301  sbth  7965  cardprc  8689  iunfictbso  8820  aceq3lem  8826  isf33lem  9071  axdc3  9159  axdclem  9224  axdc  9226  genpv  9700  ltexpri  9744  recexpr  9752  supsr  9812  hashf1lem2  13097  cvbtrcl  13579  mertens  14457  4sq  15506  isuhgr  25726  isushgr  25727  isupgr  25751  isumgr  25761  nbgraf1olem5  25974  dispcmp  29254  eulerpart  29771  ballotlemfmpn  29883  bnj66  30184  bnj1234  30335  subfacp1lem6  30421  subfacp1  30422  dfon2lem3  30934  dfon2lem7  30938  frrlem1  31024  f1omptsn  32360  ismblfin  32620  glbconxN  33682  eldioph3  36347  diophrex  36357  cbvcllem  36934  ssfiunibd  38464  isuspgr  40382  isusgr  40383  isconngr  41356  isconngr1  41357  isfrgr  41430