Theorem sbceq1d 3781

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  [wsbc 3776

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808  df-sbc 3777

This theorem is referenced by:  sbceq1dd  3782  sbcnestgfw  4417  sbcnestgf  4422  ralrnmptw  7094  ralrnmpt  7096  tfindes  7854  findes  7895  frpoins3xpg  8128  frpoins3xp3g  8129  findcard2  9166  findcard2OLD  9286  ac6sfi  9289  indexfi  9362  ac6num  10476  nn1suc  12238  uzind4s  12896  uzind4s2  12897  fzrevral  13590  fzshftral  13593  fi1uzind  14462  wrdind  14676  wrd2ind  14677  cjth  15054  prmind2  16626  isprs  18254  isdrs  18258  joinlem  18340  meetlem  18354  istos  18375  isdlat  18479  gsumvalx  18601  mndind  18745  issrg  20082  islmod  20618  quotval  26041  nn0min  32293  wrdt2ind  32384  bnj944  34247  sdclem2  36913  fdc  36916  hdmap1ffval  40969  hdmap1fval  40970  rexrabdioph  41834  2nn0ind  41986  zindbi  41987  iotasbcq  43498  prproropreud  46475