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 18	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839  df-sbc 3743

This theorem is used by:  sbceq1dd  3748  sbcnestgfw  4382  sbcnestgf  4387  ralrnmptw  7126  ralrnmpt  7128  tfindes  7908  findes  7946  frpoins3xpg  8194  frpoins3xp3g  8195  findcard2  9218  ac6sfi  9313  indexfi  9387  ac6num  10596  nn1suc  12397  uzind4s  13075  uzind4s2  13076  fzrevral  13786  fzshftral  13789  fi1uzind  14693  wrdind  14913  wrd2ind  14914  cjth  15313  prmind2  16904  isprs  18520  isdrs  18525  joinlem  18605  meetlem  18619  istos  18640  isdlat  18746  gsumvalx  18915  mndind  19074  issrg  20465  islmod  21190  quotval  26668  nn0min  33508  wrdt2ind  33612  bnj944  35679  sdclem2  38942  fdc  38945  hdmap1ffval  43118  hdmap1fval  43119  rexrabdioph  44067  2nn0ind  44218  zindbi  44219  iotasbcq  45680  prproropreud  48864