Theorem sbceq1d 3745

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  [wsbc 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-sbc 3741

This theorem is referenced by:  sbceq1dd  3746  sbcnestgfw  4373  sbcnestgf  4378  ralrnmptw  7039  ralrnmpt  7041  tfindes  7805  findes  7842  frpoins3xpg  8082  frpoins3xp3g  8083  findcard2  9089  ac6sfi  9184  indexfi  9260  ac6num  10389  nn1suc  12167  uzind4s  12821  uzind4s2  12822  fzrevral  13528  fzshftral  13531  fi1uzind  14430  wrdind  14645  wrd2ind  14646  cjth  15026  prmind2  16612  isprs  18219  isdrs  18224  joinlem  18304  meetlem  18318  istos  18339  isdlat  18445  gsumvalx  18601  mndind  18753  issrg  20123  islmod  20815  quotval  26256  nn0min  32901  wrdt2ind  33035  bnj944  35094  sdclem2  37943  fdc  37946  hdmap1ffval  42055  hdmap1fval  42056  rexrabdioph  43036  2nn0ind  43187  zindbi  43188  iotasbcq  44677  prproropreud  47755