Theorem sbceq1d 3703

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538  [wsbc 3698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-clel 2830  df-sbc 3699

This theorem is referenced by:  sbceq1dd  3704  sbcnestgfw  4318  sbcnestgf  4323  ralrnmptw  6857  ralrnmpt  6859  tfindes  7582  findes  7618  findcard2  8748  findcard2OLD  8806  ac6sfi  8808  indexfi  8878  ac6num  9952  nn1suc  11709  uzind4s  12361  uzind4s2  12362  fzrevral  13054  fzshftral  13057  fi1uzind  13920  wrdind  14144  wrd2ind  14145  cjth  14523  prmind2  16094  isprs  17619  isdrs  17623  joinlem  17700  meetlem  17714  istos  17724  isdlat  17882  gsumvalx  17965  mndind  18071  issrg  19338  islmod  19719  quotval  25000  nn0min  30670  wrdt2ind  30761  bnj944  32450  frpoins3xpg  33344  frpoins3xp3g  33345  sdclem2  35494  fdc  35497  hdmap1ffval  39405  hdmap1fval  39406  rexrabdioph  40143  2nn0ind  40294  zindbi  40295  iotasbcq  41549  prproropreud  44443