Theorem sbceq1d 3749

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsbc 3744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-sbc 3745

This theorem is referenced by:  sbceq1dd  3750  sbcnestgfw  4374  sbcnestgf  4379  ralrnmptw  7032  ralrnmpt  7034  tfindes  7803  findes  7840  frpoins3xpg  8080  frpoins3xp3g  8081  findcard2  9088  ac6sfi  9189  indexfi  9269  ac6num  10392  nn1suc  12169  uzind4s  12828  uzind4s2  12829  fzrevral  13534  fzshftral  13537  fi1uzind  14433  wrdind  14647  wrd2ind  14648  cjth  15029  prmind2  16615  isprs  18221  isdrs  18226  joinlem  18306  meetlem  18320  istos  18341  isdlat  18447  gsumvalx  18569  mndind  18721  issrg  20092  islmod  20786  quotval  26217  nn0min  32784  wrdt2ind  32914  bnj944  34924  sdclem2  37741  fdc  37744  hdmap1ffval  41794  hdmap1fval  41795  rexrabdioph  42787  2nn0ind  42938  zindbi  42939  iotasbcq  44430  prproropreud  47513