Theorem sbceq1d 3758

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-sbc 3754

This theorem is referenced by:  sbceq1dd  3759  sbcnestgfw  4384  sbcnestgf  4389  ralrnmptw  7066  ralrnmpt  7068  tfindes  7839  findes  7876  frpoins3xpg  8119  frpoins3xp3g  8120  findcard2  9128  ac6sfi  9231  indexfi  9311  ac6num  10432  nn1suc  12208  uzind4s  12867  uzind4s2  12868  fzrevral  13573  fzshftral  13576  fi1uzind  14472  wrdind  14687  wrd2ind  14688  cjth  15069  prmind2  16655  isprs  18257  isdrs  18262  joinlem  18342  meetlem  18356  istos  18377  isdlat  18481  gsumvalx  18603  mndind  18755  issrg  20097  islmod  20770  quotval  26200  nn0min  32745  wrdt2ind  32875  bnj944  34928  sdclem2  37736  fdc  37739  hdmap1ffval  41789  hdmap1fval  41790  rexrabdioph  42782  2nn0ind  42934  zindbi  42935  iotasbcq  44426  prproropreud  47510