Theorem sbceq1d 3434

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1481  [wsbc 3429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-clel 2616  df-sbc 3430

This theorem is referenced by:  sbceq1dd  3435  sbcnestgf  3986  ralrnmpt  6354  tfindes  7047  findes  7081  findcard2  8185  ac6sfi  8189  indexfi  8259  ac6num  9286  nn1suc  11026  uzind4s  11733  uzind4s2  11734  fzrevral  12409  fzshftral  12412  fi1uzind  13262  fi1uzindOLD  13268  wrdind  13458  wrd2ind  13459  cjth  13824  prmind2  15379  isprs  16911  isdrs  16915  joinlem  16992  meetlem  17006  istos  17016  isdlat  17174  gsumvalx  17251  mrcmndind  17347  issrg  18488  islmod  18848  quotval  24028  nn0min  29541  bnj944  30982  sdclem2  33509  fdc  33512  hdmap1ffval  36904  hdmap1fval  36905  rexrabdioph  37177  2nn0ind  37329  zindbi  37330  iotasbcq  38458