Theorem sbceq1d 3407

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  [wsbc 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606  df-sbc 3403

This theorem is referenced by:  sbceq1dd  3408  sbcnestgf  3947  ralrnmpt  6276  tfindes  6954  findes  6988  findcard2  8085  ac6sfi  8089  indexfi  8157  ac6num  9184  nn1suc  10918  uzind4s  11624  uzind4s2  11625  fzrevral  12294  fzshftral  12297  fi1uzind  13134  fi1uzindOLD  13140  wrdind  13328  wrd2ind  13329  cjth  13691  prmind2  15236  isprs  16753  isdrs  16757  joinlem  16834  meetlem  16848  istos  16858  isdlat  17016  gsumvalx  17093  mrcmndind  17189  issrg  18330  islmod  18690  quotval  23851  nn0min  28954  bnj944  30262  sdclem2  32708  fdc  32711  hdmap1ffval  36103  hdmap1fval  36104  rexrabdioph  36376  2nn0ind  36528  zindbi  36529  iotasbcq  37660