Theorem cbvabv 2236

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1312  {cab 2099

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106

This theorem is referenced by:  cdeqab1  2868  difjust  3036  unjust  3038  injust  3040  uniiunlem  3149  dfif3  3451  pwjust  3475  snjust  3496  intab  3764  iotajust  5043  tfrlemi1  6181  tfr1onlemaccex  6197  tfrcllemaccex  6210  frecsuc  6256  isbth  6805  nqprlu  7297  recexpr  7388  caucvgprprlemval  7438  caucvgprprlemnbj  7443  caucvgprprlemaddq  7458  caucvgprprlem1  7459  caucvgprprlem2  7460  axcaucvg  7629  mertensabs  11192  bds  12732