Theorem sbceq1d 3721

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsbc 3716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-clel 2816  df-sbc 3717

This theorem is referenced by:  sbceq1dd  3722  sbcnestgfw  4352  sbcnestgf  4357  ralrnmptw  6970  ralrnmpt  6972  tfindes  7709  findes  7749  findcard2  8947  findcard2OLD  9056  ac6sfi  9058  indexfi  9127  ac6num  10235  nn1suc  11995  uzind4s  12648  uzind4s2  12649  fzrevral  13341  fzshftral  13344  fi1uzind  14211  wrdind  14435  wrd2ind  14436  cjth  14814  prmind2  16390  isprs  18015  isdrs  18019  joinlem  18101  meetlem  18115  istos  18136  isdlat  18240  gsumvalx  18360  mndind  18466  issrg  19743  islmod  20127  quotval  25452  nn0min  31134  wrdt2ind  31225  bnj944  32918  frpoins3xpg  33787  frpoins3xp3g  33788  sdclem2  35900  fdc  35903  hdmap1ffval  39809  hdmap1fval  39810  rexrabdioph  40616  2nn0ind  40767  zindbi  40768  iotasbcq  42055  prproropreud  44961