Theorem sbceq1d 3728

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  [wsbc 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-clel 2814  df-sbc 3724

This theorem is referenced by:  sbceq1dd  3729  sbcnestgfw  4349  sbcnestgf  4354  ralrnmptw  7035  ralrnmpt  7037  tfindes  7803  findes  7840  frpoins3xpg  8080  frpoins3xp3g  8081  findcard2  9089  ac6sfi  9184  indexfi  9260  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  20854  quotval  26276  nn0min  32913  wrdt2ind  33032  bnj944  35120  sdclem2  38109  fdc  38112  hdmap1ffval  42287  hdmap1fval  42288  rexrabdioph  43239  2nn0ind  43390  zindbi  43391  iotasbcq  44880  prproropreud  47984