Theorem sbceq1d 3734

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-sbc 3730

This theorem is referenced by:  sbceq1dd  3735  sbcnestgfw  4362  sbcnestgf  4367  ralrnmptw  7040  ralrnmpt  7042  tfindes  7807  findes  7844  frpoins3xpg  8083  frpoins3xp3g  8084  findcard2  9092  ac6sfi  9187  indexfi  9263  ac6num  10392  nn1suc  12187  uzind4s  12849  uzind4s2  12850  fzrevral  13557  fzshftral  13560  fi1uzind  14460  wrdind  14675  wrd2ind  14676  cjth  15056  prmind2  16645  isprs  18253  isdrs  18258  joinlem  18338  meetlem  18352  istos  18373  isdlat  18479  gsumvalx  18635  mndind  18787  issrg  20160  islmod  20850  quotval  26269  nn0min  32909  wrdt2ind  33028  bnj944  35096  sdclem2  38077  fdc  38080  hdmap1ffval  42255  hdmap1fval  42256  rexrabdioph  43240  2nn0ind  43391  zindbi  43392  iotasbcq  44881  prproropreud  47981