Theorem sbceq1d 3758

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-clel 2844  df-sbc 3754

This theorem is referenced by:  sbceq1dd  3759  sbcnestgfw  4384  sbcnestgf  4389  ralrnmptw  7087  ralrnmpt  7089  tfindes  7855  findes  7893  frpoins3xpg  8132  frpoins3xp3g  8133  findcard2  9145  ac6sfi  9240  indexfi  9313  ac6num  10459  nn1suc  12251  uzind4s  12928  uzind4s2  12929  fzrevral  13636  fzshftral  13639  fi1uzind  14540  wrdind  14755  wrd2ind  14756  cjth  15150  prmind2  16739  isprs  18348  isdrs  18353  joinlem  18433  meetlem  18447  istos  18468  isdlat  18574  gsumvalx  18730  mndind  18883  issrg  20266  islmod  20959  quotval  26418  nn0min  33102  wrdt2ind  33210  bnj944  35267  sdclem2  38276  fdc  38279  hdmap1ffval  42454  hdmap1fval  42455  rexrabdioph  43406  2nn0ind  43557  zindbi  43558  iotasbcq  45031  prproropreud  48140