Theorem sbceq1d 3775

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsbc 3770

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-clel 2810  df-sbc 3771

This theorem is referenced by:  sbceq1dd  3776  sbcnestgfw  4401  sbcnestgf  4406  ralrnmptw  7089  ralrnmpt  7091  tfindes  7863  findes  7901  frpoins3xpg  8144  frpoins3xp3g  8145  findcard2  9183  ac6sfi  9297  indexfi  9377  ac6num  10498  nn1suc  12267  uzind4s  12929  uzind4s2  12930  fzrevral  13634  fzshftral  13637  fi1uzind  14530  wrdind  14745  wrd2ind  14746  cjth  15127  prmind2  16709  isprs  18313  isdrs  18318  joinlem  18398  meetlem  18412  istos  18433  isdlat  18537  gsumvalx  18659  mndind  18811  issrg  20153  islmod  20826  quotval  26257  nn0min  32804  wrdt2ind  32934  bnj944  34974  sdclem2  37771  fdc  37774  hdmap1ffval  41819  hdmap1fval  41820  rexrabdioph  42792  2nn0ind  42944  zindbi  42945  iotasbcq  44436  prproropreud  47503