Theorem sbceq1a 3446

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

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   [wsb 1880   [.wsbc 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-sbc 3436

This theorem is referenced by:  sbceq2a  3447  elrabsf  3474  cbvralcsf  3565  rabsnifsb  4257  euotd  4975  wfisg  5715  elfvmptrab1  6305  ralrnmpt  6368  riotass2  6638  riotass  6639  oprabv  6703  elovmpt2rab  6880  elovmpt2rab1  6881  ovmpt3rabdm  6892  elovmpt3rab1  6893  tfindes  7062  sbcopeq1a  7220  mpt2xopoveq  7345  findcard2  8200  ac6sfi  8204  indexfi  8274  nn0ind-raph  11477  fzrevral  12425  wrdind  13476  wrd2ind  13477  prmind2  15398  elmptrab  21630  isfildlem  21661  gropd  25923  grstructd  25924  vtocl2d  29314  ifeqeqx  29361  bnj919  30837  bnj976  30848  bnj1468  30916  bnj110  30928  bnj150  30946  bnj151  30947  bnj607  30986  bnj873  30994  bnj849  30995  bnj1388  31101  setinds  31683  dfon2lem1  31688  tfisg  31716  frinsg  31742  indexdom  33529  sdclem2  33538  sdclem1  33539  fdc1  33542  riotasv2s  34244  elimhyps  34247  sbccomieg  37357  rexrabdioph  37358  rexfrabdioph  37359  aomclem6  37629  pm13.13a  38608  pm13.13b  38609  pm13.14  38610  tratrb  38746  uzwo4  39221