Theorem cbvabv 2747

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  {cab 2608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615

This theorem is referenced by:  cdeqab1  3427  difjust  3576  unjust  3578  injust  3580  uniiunlem  3691  dfif3  4100  pwjust  4159  snjust  4176  intab  4507  intabs  4825  iotajust  5850  wfrlem1  7414  sbth  8080  cardprc  8806  iunfictbso  8937  aceq3lem  8943  isf33lem  9188  axdc3  9276  axdclem  9341  axdc  9343  genpv  9821  ltexpri  9865  recexpr  9873  supsr  9933  hashf1lem2  13240  cvbtrcl  13731  mertens  14618  4sq  15668  isuhgr  25955  isushgr  25956  isupgr  25979  isumgr  25990  isuspgr  26047  isusgr  26048  isconngr  27049  isconngr1  27050  isfrgr  27122  dispcmp  29926  eulerpart  30444  ballotlemfmpn  30556  bnj66  30930  bnj1234  31081  subfacp1lem6  31167  subfacp1  31168  dfon2lem3  31690  dfon2lem7  31694  frrlem1  31780  nosupdm  31850  f1omptsn  33184  ismblfin  33450  glbconxN  34664  eldioph3  37329  diophrex  37339  cbvcllem  37915  ssfiunibd  39523