Theorem sbceq1d 3440

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483  [wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  sbceq1dd  3441  sbcnestgf  3995  ralrnmpt  6368  tfindes  7062  findes  7096  findcard2  8200  ac6sfi  8204  indexfi  8274  ac6num  9301  nn1suc  11041  uzind4s  11748  uzind4s2  11749  fzrevral  12425  fzshftral  12428  fi1uzind  13279  fi1uzindOLD  13285  wrdind  13476  wrd2ind  13477  cjth  13843  prmind2  15398  isprs  16930  isdrs  16934  joinlem  17011  meetlem  17025  istos  17035  isdlat  17193  gsumvalx  17270  mrcmndind  17366  issrg  18507  islmod  18867  quotval  24047  nn0min  29567  bnj944  31008  sdclem2  33538  fdc  33541  hdmap1ffval  37085  hdmap1fval  37086  rexrabdioph  37358  2nn0ind  37510  zindbi  37511  iotasbcq  38638