Theorem sbceq1d 3711

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1522  [wsbc 3706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-clel 2863  df-sbc 3707

This theorem is referenced by:  sbceq1dd  3712  sbcnestgf  4290  ralrnmpt  6725  tfindes  7433  findes  7468  findcard2  8604  ac6sfi  8608  indexfi  8678  ac6num  9747  nn1suc  11507  uzind4s  12157  uzind4s2  12158  fzrevral  12842  fzshftral  12845  fi1uzind  13701  wrdind  13920  wrd2ind  13921  cjth  14296  prmind2  15858  isprs  17369  isdrs  17373  joinlem  17450  meetlem  17464  istos  17474  isdlat  17632  gsumvalx  17709  mndind  17805  issrg  18947  islmod  19328  quotval  24564  nn0min  30221  wrdt2ind  30306  bnj944  31826  sdclem2  34549  fdc  34552  hdmap1ffval  38462  hdmap1fval  38463  rexrabdioph  38876  2nn0ind  39027  zindbi  39028  iotasbcq  40307  prproropreud  43153