Theorem sbceq1d 3782

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1540  [wsbc 3777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809  df-sbc 3778

This theorem is referenced by:  sbceq1dd  3783  sbcnestgfw  4418  sbcnestgf  4423  ralrnmptw  7095  ralrnmpt  7097  tfindes  7856  findes  7897  frpoins3xpg  8131  frpoins3xp3g  8132  findcard2  9170  findcard2OLD  9290  ac6sfi  9293  indexfi  9366  ac6num  10480  nn1suc  12241  uzind4s  12899  uzind4s2  12900  fzrevral  13593  fzshftral  13596  fi1uzind  14465  wrdind  14679  wrd2ind  14680  cjth  15057  prmind2  16629  isprs  18260  isdrs  18264  joinlem  18346  meetlem  18360  istos  18381  isdlat  18485  gsumvalx  18607  mndind  18751  issrg  20089  islmod  20706  quotval  26143  nn0min  32458  wrdt2ind  32549  bnj944  34412  sdclem2  37073  fdc  37076  hdmap1ffval  41129  hdmap1fval  41130  rexrabdioph  41994  2nn0ind  42146  zindbi  42147  iotasbcq  43658  prproropreud  46635