Theorem sbceq1d 3747

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsbc 3742

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-sbc 3743

This theorem is referenced by:  sbceq1dd  3748  sbcnestgfw  4375  sbcnestgf  4380  ralrnmptw  7048  ralrnmpt  7050  tfindes  7815  findes  7852  frpoins3xpg  8092  frpoins3xp3g  8093  findcard2  9101  ac6sfi  9196  indexfi  9272  ac6num  10401  nn1suc  12179  uzind4s  12833  uzind4s2  12834  fzrevral  13540  fzshftral  13543  fi1uzind  14442  wrdind  14657  wrd2ind  14658  cjth  15038  prmind2  16624  isprs  18231  isdrs  18236  joinlem  18316  meetlem  18330  istos  18351  isdlat  18457  gsumvalx  18613  mndind  18765  issrg  20135  islmod  20827  quotval  26268  nn0min  32911  wrdt2ind  33045  bnj944  35113  sdclem2  37990  fdc  37993  hdmap1ffval  42168  hdmap1fval  42169  rexrabdioph  43148  2nn0ind  43299  zindbi  43300  iotasbcq  44789  prproropreud  47866