Theorem sbceq1d 3730

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1548  [wsbc 3725

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788  df-cleq 2733  df-clel 2816  df-sbc 3726

This theorem is referenced by:  sbceq1dd  3731  sbcnestgfw  4352  sbcnestgf  4357  ralrnmptw  7039  ralrnmpt  7041  tfindes  7807  findes  7844  frpoins3xpg  8084  frpoins3xp3g  8085  findcard2  9093  ac6sfi  9188  indexfi  9264  ac6num  10396  nn1suc  12191  uzind4s  12853  uzind4s2  12854  fzrevral  13561  fzshftral  13564  fi1uzind  14464  wrdind  14679  wrd2ind  14680  cjth  15060  prmind2  16649  isprs  18257  isdrs  18262  joinlem  18342  meetlem  18356  istos  18377  isdlat  18483  gsumvalx  18639  mndind  18791  issrg  20164  islmod  20858  quotval  26280  nn0min  32917  wrdt2ind  33036  bnj944  35135  sdclem2  38124  fdc  38127  hdmap1ffval  42302  hdmap1fval  42303  rexrabdioph  43254  2nn0ind  43405  zindbi  43406  iotasbcq  44895  prproropreud  47998