Theorem sbceq1d 3056

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 3053	. 2 |- ( A = B -> ( [. A / x ]. ps <-> [. B / x ]. ps ) )
3	1, 2	syl 14	1 |- ( ph -> ( [. A / x ]. ps <-> [. B / x ]. ps ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   [.wsbc 3051

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-sbc 3052

This theorem is used by:  sbceq1dd  3057  rexrnmpt  5854  findcard2  7197  findcard2s  7198  ac6sfi  7206  nn1suc  9332  uzind4s  10006  uzind4s2  10007  fzrevral  10529  fzshftral  10532  wrdind  11516  wrd2ind  11517  cjth  11633  prmind2  12923  issrg  14376  islmod  14736  isassa  15111  bj-bdfindes  17180  bj-findes  17212