Theorem sbceq1d 3776

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1533  [wsbc 3771

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-clel 2893  df-sbc 3772

This theorem is referenced by:  sbceq1dd  3777  sbcnestgfw  4369  sbcnestgf  4374  ralrnmptw  6859  ralrnmpt  6861  tfindes  7576  findes  7611  findcard2  8757  ac6sfi  8761  indexfi  8831  ac6num  9900  nn1suc  11658  uzind4s  12307  uzind4s2  12308  fzrevral  12991  fzshftral  12994  fi1uzind  13854  wrdind  14083  wrd2ind  14084  cjth  14461  prmind2  16028  isprs  17539  isdrs  17543  joinlem  17620  meetlem  17634  istos  17644  isdlat  17802  gsumvalx  17885  mndind  17991  issrg  19256  islmod  19637  quotval  24880  nn0min  30536  wrdt2ind  30627  bnj944  32210  sdclem2  35016  fdc  35019  hdmap1ffval  38930  hdmap1fval  38931  rexrabdioph  39389  2nn0ind  39540  zindbi  39541  iotasbcq  40767  prproropreud  43670