Theorem sbceq1d 3751

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

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-clel 2840  df-sbc 3747

This theorem is used by:  sbceq1dd  3752  sbcnestgfw  4386  sbcnestgf  4391  ralrnmptw  7093  ralrnmpt  7095  tfindes  7861  findes  7899  frpoins3xpg  8138  frpoins3xp3g  8139  findcard2  9152  ac6sfi  9247  indexfi  9320  ac6num  10474  nn1suc  12266  uzind4s  12943  uzind4s2  12944  fzrevral  13652  fzshftral  13655  fi1uzind  14557  wrdind  14776  wrd2ind  14777  cjth  15173  prmind2  16760  isprs  18369  isdrs  18374  joinlem  18454  meetlem  18468  istos  18489  isdlat  18595  gsumvalx  18755  mndind  18910  issrg  20293  islmod  21014  quotval  26482  nn0min  33194  wrdt2ind  33298  bnj944  35350  sdclem2  38426  fdc  38429  hdmap1ffval  42602  hdmap1fval  42603  rexrabdioph  43554  2nn0ind  43705  zindbi  43706  iotasbcq  45179  prproropreud  48291