Theorem sbceq1d 3592

Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)

Hypothesis

Ref	Expression
sbceq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
sbceq1d	⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))

Proof of Theorem sbceq1d

Step	Hyp	Ref	Expression
1		sbceq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		dfsbcq 3589	. 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631  [wsbc 3587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767  df-sbc 3588

This theorem is referenced by:  sbceq1dd  3593  sbcnestgf  4140  ralrnmpt  6513  tfindes  7213  findes  7247  findcard2  8360  ac6sfi  8364  indexfi  8434  ac6num  9507  nn1suc  11247  uzind4s  11955  uzind4s2  11956  fzrevral  12632  fzshftral  12635  fi1uzind  13481  wrdind  13685  wrd2ind  13686  cjth  14051  prmind2  15605  isprs  17138  isdrs  17142  joinlem  17219  meetlem  17233  istos  17243  isdlat  17401  gsumvalx  17478  mrcmndind  17574  issrg  18715  islmod  19077  quotval  24267  nn0min  29907  bnj944  31346  sdclem2  33868  fdc  33871  hdmap1ffval  37603  hdmap1fval  37604  rexrabdioph  37882  2nn0ind  38034  zindbi  38035  iotasbcq  39162