Theorem sbceq1d 3782

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541  [wsbc 3777

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810  df-sbc 3778

This theorem is referenced by:  sbceq1dd  3783  sbcnestgfw  4418  sbcnestgf  4423  ralrnmptw  7095  ralrnmpt  7097  tfindes  7851  findes  7892  frpoins3xpg  8125  frpoins3xp3g  8126  findcard2  9163  findcard2OLD  9283  ac6sfi  9286  indexfi  9359  ac6num  10473  nn1suc  12233  uzind4s  12891  uzind4s2  12892  fzrevral  13585  fzshftral  13588  fi1uzind  14457  wrdind  14671  wrd2ind  14672  cjth  15049  prmind2  16621  isprs  18249  isdrs  18253  joinlem  18335  meetlem  18349  istos  18370  isdlat  18474  gsumvalx  18594  mndind  18708  issrg  20010  islmod  20474  quotval  25804  nn0min  32021  wrdt2ind  32112  bnj944  33944  sdclem2  36605  fdc  36608  hdmap1ffval  40661  hdmap1fval  40662  rexrabdioph  41522  2nn0ind  41674  zindbi  41675  iotasbcq  43186  prproropreud  46167