Theorem sbceq1d 3638

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 3635	. 2 ⊢ (𝐴 = 𝐵 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))
3	1, 2	syl 17	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  [wsbc 3633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2799  df-clel 2802  df-sbc 3634

This theorem is referenced by:  sbceq1dd  3639  sbcnestgf  4192  ralrnmpt  6590  tfindes  7292  findes  7326  findcard2  8439  ac6sfi  8443  indexfi  8513  ac6num  9586  nn1suc  11326  uzind4s  11966  uzind4s2  11967  fzrevral  12648  fzshftral  12651  fi1uzind  13496  wrdind  13700  wrd2ind  13701  cjth  14066  prmind2  15616  isprs  17135  isdrs  17139  joinlem  17216  meetlem  17230  istos  17240  isdlat  17398  gsumvalx  17475  mrcmndind  17571  issrg  18709  islmod  19071  quotval  24261  nn0min  29894  bnj944  31331  sdclem2  33849  fdc  33852  hdmap1ffval  37576  hdmap1fval  37577  rexrabdioph  37860  2nn0ind  38011  zindbi  38012  iotasbcq  39137