Theorem sbceq1a 2964

Description: Equality theorem for class substitution. Class version of sbequ12 1764. (Contributed by NM, 26-Sep-2003.)

Assertion

Ref	Expression
sbceq1a	|- ( x = A -> ( ph <-> [. A / x ]. ph ) )

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 1767	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 2958	. 2 |- ( x = A -> ( [ x / x ] ph <-> [. A / x ]. ph ) )
3	1, 2	bitr3id 193	1 |- ( x = A -> ( ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1348   [wsb 1755   [.wsbc 2955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-sbc 2956

This theorem is referenced by:  sbceq2a  2965  elrabsf  2993  cbvralcsf  3111  cbvrexcsf  3112  euotd  4239  omsinds  4606  elfvmptrab1  5590  ralrnmpt  5638  rexrnmpt  5639  riotass2  5835  riotass  5836  sbcopeq1a  6166  mpoxopoveq  6219  findcard2  6867  findcard2s  6868  ac6sfi  6876  dcfi  6958  indpi  7304  nn0ind-raph  9329  indstr  9552  fzrevral  10061  exfzdc  10196  uzsinds  10398  zsupcllemstep  11900  infssuzex  11904  prmind2  12074  bj-intabssel  13824  bj-bdfindes  13984  bj-findes  14016