Theorem sbceq1d 3750

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  [wsbc 3745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-sbc 3746

This theorem is referenced by:  sbceq1dd  3751  sbcnestgfw  4387  sbcnestgf  4392  ralrnmptw  7091  ralrnmpt  7093  tfindes  7860  findes  7898  frpoins3xpg  8137  frpoins3xp3g  8138  findcard2  9150  ac6sfi  9245  indexfi  9318  ac6num  10464  nn1suc  12256  uzind4s  12933  uzind4s2  12934  fzrevral  13642  fzshftral  13645  fi1uzind  14546  wrdind  14761  wrd2ind  14762  cjth  15156  prmind2  16744  isprs  18353  isdrs  18358  joinlem  18438  meetlem  18452  istos  18473  isdlat  18579  gsumvalx  18735  mndind  18888  issrg  20271  islmod  20966  quotval  26434  nn0min  33146  wrdt2ind  33254  bnj944  35307  sdclem2  38374  fdc  38377  hdmap1ffval  42550  hdmap1fval  42551  rexrabdioph  43504  2nn0ind  43655  zindbi  43656  iotasbcq  45129  prproropreud  48241