Theorem sbceq1d 3747

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836  df-sbc 3743

This theorem is referenced by:  sbceq1dd  3748  sbcnestgfw  4372  sbcnestgf  4377  ralrnmptw  7070  ralrnmpt  7072  tfindes  7838  findes  7876  frpoins3xpg  8114  frpoins3xp3g  8115  findcard2  9127  ac6sfi  9222  indexfi  9297  ac6num  10430  nn1suc  12226  uzind4s  12903  uzind4s2  12904  fzrevral  13611  fzshftral  13614  fi1uzind  14514  wrdind  14729  wrd2ind  14730  cjth  15121  prmind2  16710  isprs  18319  isdrs  18324  joinlem  18404  meetlem  18418  istos  18439  isdlat  18545  gsumvalx  18701  mndind  18853  issrg  20225  islmod  20919  quotval  26344  nn0min  32984  wrdt2ind  33092  bnj944  35194  sdclem2  38202  fdc  38205  hdmap1ffval  42380  hdmap1fval  42381  rexrabdioph  43332  2nn0ind  43483  zindbi  43484  iotasbcq  44973  prproropreud  48076