Theorem sbceq1d 3744

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-sbc 3740

This theorem is used by:  sbceq1dd  3745  sbcnestgfw  4379  sbcnestgf  4384  ralrnmptw  7092  ralrnmpt  7094  tfindes  7872  findes  7910  frpoins3xpg  8150  frpoins3xp3g  8151  findcard2  9173  ac6sfi  9268  indexfi  9342  ac6num  10550  nn1suc  12350  uzind4s  13028  uzind4s2  13029  fzrevral  13739  fzshftral  13742  fi1uzind  14645  wrdind  14864  wrd2ind  14865  cjth  15263  prmind2  16853  isprs  18463  isdrs  18468  joinlem  18548  meetlem  18562  istos  18583  isdlat  18689  gsumvalx  18858  mndind  19017  issrg  20407  islmod  21132  quotval  26606  nn0min  33405  wrdt2ind  33509  bnj944  35561  sdclem2  38656  fdc  38659  hdmap1ffval  42832  hdmap1fval  42833  rexrabdioph  43780  2nn0ind  43931  zindbi  43932  iotasbcq  45405  prproropreud  48560