Theorem sbceq1d 3733

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsbc 3728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  sbceq1dd  3734  sbcnestgfw  4361  sbcnestgf  4366  ralrnmptw  7046  ralrnmpt  7048  tfindes  7814  findes  7851  frpoins3xpg  8090  frpoins3xp3g  8091  findcard2  9099  ac6sfi  9194  indexfi  9270  ac6num  10401  nn1suc  12196  uzind4s  12858  uzind4s2  12859  fzrevral  13566  fzshftral  13569  fi1uzind  14469  wrdind  14684  wrd2ind  14685  cjth  15065  prmind2  16654  isprs  18262  isdrs  18267  joinlem  18347  meetlem  18361  istos  18382  isdlat  18488  gsumvalx  18644  mndind  18796  issrg  20169  islmod  20859  quotval  26258  nn0min  32894  wrdt2ind  33013  bnj944  35080  sdclem2  38063  fdc  38066  hdmap1ffval  42241  hdmap1fval  42242  rexrabdioph  43222  2nn0ind  43373  zindbi  43374  iotasbcq  44863  prproropreud  47969