Theorem sbceq1d 3792

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539  [wsbc 3787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-clel 2815  df-sbc 3788

This theorem is referenced by:  sbceq1dd  3793  sbcnestgfw  4420  sbcnestgf  4425  ralrnmptw  7113  ralrnmpt  7115  tfindes  7885  findes  7923  frpoins3xpg  8166  frpoins3xp3g  8167  findcard2  9205  ac6sfi  9321  indexfi  9401  ac6num  10520  nn1suc  12289  uzind4s  12951  uzind4s2  12952  fzrevral  13653  fzshftral  13656  fi1uzind  14547  wrdind  14761  wrd2ind  14762  cjth  15143  prmind2  16723  isprs  18343  isdrs  18348  joinlem  18429  meetlem  18443  istos  18464  isdlat  18568  gsumvalx  18690  mndind  18842  issrg  20186  islmod  20863  quotval  26335  nn0min  32823  wrdt2ind  32939  bnj944  34953  sdclem2  37750  fdc  37753  hdmap1ffval  41798  hdmap1fval  41799  rexrabdioph  42810  2nn0ind  42962  zindbi  42963  iotasbcq  44461  prproropreud  47501