Theorem sbceq1d 3768

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539  [wsbc 3763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-clel 2808  df-sbc 3764

This theorem is referenced by:  sbceq1dd  3769  sbcnestgfw  4394  sbcnestgf  4399  ralrnmptw  7080  ralrnmpt  7082  tfindes  7852  findes  7890  frpoins3xpg  8133  frpoins3xp3g  8134  findcard2  9172  ac6sfi  9286  indexfi  9366  ac6num  10485  nn1suc  12254  uzind4s  12916  uzind4s2  12917  fzrevral  13618  fzshftral  13621  fi1uzind  14513  wrdind  14727  wrd2ind  14728  cjth  15109  prmind2  16689  isprs  18293  isdrs  18298  joinlem  18378  meetlem  18392  istos  18413  isdlat  18517  gsumvalx  18639  mndind  18791  issrg  20133  islmod  20806  quotval  26237  nn0min  32732  wrdt2ind  32848  bnj944  34890  sdclem2  37687  fdc  37690  hdmap1ffval  41735  hdmap1fval  41736  rexrabdioph  42742  2nn0ind  42894  zindbi  42895  iotasbcq  44387  prproropreud  47441