Theorem sbceq1d 3780

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1536  [wsbc 3775

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-cleq 2817  df-clel 2896  df-sbc 3776

This theorem is referenced by:  sbceq1dd  3781  sbcnestgfw  4373  sbcnestgf  4378  ralrnmptw  6863  ralrnmpt  6865  tfindes  7580  findes  7615  findcard2  8761  ac6sfi  8765  indexfi  8835  ac6num  9904  nn1suc  11662  uzind4s  12311  uzind4s2  12312  fzrevral  12995  fzshftral  12998  fi1uzind  13858  wrdind  14087  wrd2ind  14088  cjth  14465  prmind2  16032  isprs  17543  isdrs  17547  joinlem  17624  meetlem  17638  istos  17648  isdlat  17806  gsumvalx  17889  mndind  17995  issrg  19260  islmod  19641  quotval  24884  nn0min  30540  wrdt2ind  30631  bnj944  32214  sdclem2  35021  fdc  35024  hdmap1ffval  38935  hdmap1fval  38936  rexrabdioph  39397  2nn0ind  39548  zindbi  39549  iotasbcq  40775  prproropreud  43678