Theorem sbceq1a 3290

Description: Equality theorem for class substitution. Class version of sbequ12 2094. (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 2097	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 3282	. 2 |- ( x = A -> ( [ x / x ] ph <-> [. A / x ]. ph ) )
3	1, 2	syl5bbr 267	1 |- ( x = A -> ( ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1455   [wsb 1808   [.wsbc 3279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-12 1944  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-sbc 3280

This theorem is referenced by:  sbceq2a  3291  elrabsf  3318  cbvralcsf  3407  rabsnifsb  4053  euotd  4719  wfisg  5438  elfvmptrab1  5998  ralrnmpt  6059  riotass2  6308  riotass  6309  oprabv  6371  elovmpt2rab  6547  elovmpt2rab1  6548  ovmpt3rabdm  6558  elovmpt3rab1  6559  tfindes  6721  sbcopeq1a  6877  mpt2xopoveq  6997  findcard2  7842  ac6sfi  7846  indexfi  7913  nn0ind-raph  11069  fzrevral  11914  wrdind  12876  wrd2ind  12877  prmind2  14690  elmptrab  20897  isfildlem  20927  vtocl2d  28165  ifeqeqx  28213  bnj919  29628  bnj976  29639  bnj1468  29707  bnj110  29719  bnj150  29737  bnj151  29738  bnj607  29777  bnj873  29785  bnj849  29786  bnj1388  29892  setinds  30474  dfon2lem1  30479  tfisg  30507  frinsg  30533  indexdom  32107  sdclem2  32117  sdclem1  32118  fdc1  32121  riotasv2s  32576  sbccomieg  35682  rexrabdioph  35683  rexfrabdioph  35684  aomclem6  35963  pm13.13a  36803  pm13.13b  36804  pm13.14  36805  tratrb  36942  uzwo4  37431  gropd  39275  grstructd  39276