Theorem sbceq1d 3010

Description: Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.)

Hypothesis

Ref	Expression
sbceq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
sbceq1d	|- ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ps ) )

Proof of Theorem sbceq1d

Step	Hyp	Ref	Expression
1		sbceq1d.1	. 2 |- ( ph -> A = B )
2		dfsbcq 3007	. 2 |- ( A = B -> ( [. A / x ]. ps <-> [. B / x ]. ps ) )
3	1, 2	syl 14	1 |- ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ps ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1373   [.wsbc 3005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203  df-sbc 3006

This theorem is referenced by:  sbceq1dd  3011  rexrnmpt  5746  findcard2  7012  findcard2s  7013  ac6sfi  7021  nn1suc  9090  uzind4s  9746  uzind4s2  9747  fzrevral  10262  fzshftral  10265  wrdind  11213  wrd2ind  11214  cjth  11272  prmind2  12557  issrg  13842  islmod  14168  bj-bdfindes  16084  bj-findes  16116