Theorem sbceq1d 3809

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  sbceq1dd  3810  sbcnestgfw  4444  sbcnestgf  4449  ralrnmptw  7128  ralrnmpt  7130  tfindes  7900  findes  7940  frpoins3xpg  8181  frpoins3xp3g  8182  findcard2  9230  ac6sfi  9348  indexfi  9430  ac6num  10548  nn1suc  12315  uzind4s  12973  uzind4s2  12974  fzrevral  13669  fzshftral  13672  fi1uzind  14556  wrdind  14770  wrd2ind  14771  cjth  15152  prmind2  16732  isprs  18367  isdrs  18371  joinlem  18453  meetlem  18467  istos  18488  isdlat  18592  gsumvalx  18714  mndind  18863  issrg  20215  islmod  20884  quotval  26352  nn0min  32824  wrdt2ind  32920  bnj944  34914  sdclem2  37702  fdc  37705  hdmap1ffval  41752  hdmap1fval  41753  rexrabdioph  42750  2nn0ind  42902  zindbi  42903  iotasbcq  44406  prproropreud  47383