Theorem sbceq1d 3755

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

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

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 3751

This theorem is referenced by:  sbceq1dd  3756  sbcnestgfw  4380  sbcnestgf  4385  ralrnmptw  7048  ralrnmpt  7050  tfindes  7819  findes  7856  frpoins3xpg  8096  frpoins3xp3g  8097  findcard2  9105  ac6sfi  9207  indexfi  9287  ac6num  10408  nn1suc  12184  uzind4s  12843  uzind4s2  12844  fzrevral  13549  fzshftral  13552  fi1uzind  14448  wrdind  14663  wrd2ind  14664  cjth  15045  prmind2  16631  isprs  18233  isdrs  18238  joinlem  18318  meetlem  18332  istos  18353  isdlat  18457  gsumvalx  18579  mndind  18731  issrg  20073  islmod  20746  quotval  26176  nn0min  32718  wrdt2ind  32848  bnj944  34901  sdclem2  37709  fdc  37712  hdmap1ffval  41762  hdmap1fval  41763  rexrabdioph  42755  2nn0ind  42907  zindbi  42908  iotasbcq  44399  prproropreud  47483