Theorem cbvabv 2744

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1480  {cab 2607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614

This theorem is referenced by:  cdeqab1  3414  difjust  3562  unjust  3564  injust  3566  uniiunlem  3675  dfif3  4078  pwjust  4137  snjust  4154  intab  4479  intabs  4795  iotajust  5819  wfrlem1  7374  sbth  8040  cardprc  8766  iunfictbso  8897  aceq3lem  8903  isf33lem  9148  axdc3  9236  axdclem  9301  axdc  9303  genpv  9781  ltexpri  9825  recexpr  9833  supsr  9893  hashf1lem2  13194  cvbtrcl  13681  mertens  14562  4sq  15611  isuhgr  25885  isushgr  25886  isupgr  25909  isumgr  25919  isuspgr  25974  isusgr  25975  isconngr  26949  isconngr1  26950  isfrgr  27022  dispcmp  29750  eulerpart  30267  ballotlemfmpn  30379  bnj66  30691  bnj1234  30842  subfacp1lem6  30928  subfacp1  30929  dfon2lem3  31444  dfon2lem7  31448  frrlem1  31534  f1omptsn  32855  ismblfin  33121  glbconxN  34183  eldioph3  36848  diophrex  36858  cbvcllem  37435  ssfiunibd  39022