Theorem sbceq1d 3589

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

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1629  [wsbc 3584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1868  ax-4 1883  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2152  ax-ext 2749

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1851  df-cleq 2762  df-clel 2765  df-sbc 3585

This theorem is referenced by:  sbceq1dd  3590  sbcnestgf  4136  ralrnmpt  6510  tfindes  7207  findes  7241  findcard2  8354  ac6sfi  8358  indexfi  8428  ac6num  9501  nn1suc  11241  uzind4s  11949  uzind4s2  11950  fzrevral  12631  fzshftral  12634  fi1uzind  13484  wrdind  13688  wrd2ind  13689  cjth  14054  prmind2  15611  isprs  17144  isdrs  17148  joinlem  17225  meetlem  17239  istos  17249  isdlat  17407  gsumvalx  17484  mrcmndind  17580  issrg  18721  islmod  19083  quotval  24273  nn0min  29908  bnj944  31347  sdclem2  33870  fdc  33873  hdmap1ffval  37605  hdmap1fval  37606  rexrabdioph  37884  2nn0ind  38036  zindbi  38037  iotasbcq  39164