Theorem sbceq1d 3033

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 3030	. 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 1395   [.wsbc 3028

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-sbc 3029

This theorem is referenced by:  sbceq1dd  3034  rexrnmpt  5778  findcard2  7051  findcard2s  7052  ac6sfi  7060  nn1suc  9129  uzind4s  9785  uzind4s2  9786  fzrevral  10301  fzshftral  10304  wrdind  11254  wrd2ind  11255  cjth  11357  prmind2  12642  issrg  13928  islmod  14255  bj-bdfindes  16312  bj-findes  16344