Theorem sbceq1d 3742

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsbc 3737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808  df-sbc 3738

This theorem is referenced by:  sbceq1dd  3743  sbcnestgfw  4370  sbcnestgf  4375  ralrnmptw  7036  ralrnmpt  7038  tfindes  7802  findes  7839  frpoins3xpg  8079  frpoins3xp3g  8080  findcard2  9085  ac6sfi  9179  indexfi  9255  ac6num  10381  nn1suc  12158  uzind4s  12812  uzind4s2  12813  fzrevral  13519  fzshftral  13522  fi1uzind  14421  wrdind  14636  wrd2ind  14637  cjth  15017  prmind2  16603  isprs  18210  isdrs  18215  joinlem  18295  meetlem  18309  istos  18330  isdlat  18436  gsumvalx  18592  mndind  18744  issrg  20114  islmod  20806  quotval  26247  nn0min  32829  wrdt2ind  32963  bnj944  35022  sdclem2  37855  fdc  37858  hdmap1ffval  41967  hdmap1fval  41968  rexrabdioph  42951  2nn0ind  43102  zindbi  43103  iotasbcq  44593  prproropreud  47671