Theorem sbceq1d 3743

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-clel 2835  df-sbc 3739

This theorem is used by:  sbceq1dd  3744  sbcnestgfw  4378  sbcnestgf  4383  ralrnmptw  7095  ralrnmpt  7097  tfindes  7875  findes  7913  frpoins3xpg  8160  frpoins3xp3g  8161  findcard2  9184  ac6sfi  9279  indexfi  9353  ac6num  10561  nn1suc  12361  uzind4s  13039  uzind4s2  13040  fzrevral  13750  fzshftral  13753  fi1uzind  14656  wrdind  14876  wrd2ind  14877  cjth  15276  prmind2  16866  isprs  18476  isdrs  18481  joinlem  18561  meetlem  18575  istos  18596  isdlat  18702  gsumvalx  18871  mndind  19030  issrg  20420  islmod  21145  quotval  26619  nn0min  33459  wrdt2ind  33563  bnj944  35615  sdclem2  38770  fdc  38773  hdmap1ffval  42946  hdmap1fval  42947  rexrabdioph  43895  2nn0ind  44046  zindbi  44047  iotasbcq  45514  prproropreud  48685