Theorem sbceq1a 3310

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

Syntax hints:   -> wi 4   <-> wb 187   = wceq 1437   [wsb 1786   [.wsbc 3299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-12 1905  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-sbc 3300

This theorem is referenced by:  sbceq2a  3311  elrabsf  3338  cbvralcsf  3427  rabsnifsb  4065  euotd  4717  wfisg  5430  elfvmptrab1  5982  ralrnmpt  6042  riotass2  6289  riotass  6290  oprabv  6349  elovmpt2rab  6525  elovmpt2rab1  6526  ovmpt3rabdm  6536  elovmpt3rab1  6537  tfindes  6699  sbcopeq1a  6855  mpt2xopoveq  6969  findcard2  7813  ac6sfi  7817  indexfi  7884  nn0ind-raph  11035  fzrevral  11879  wrdind  12823  wrd2ind  12824  prmind2  14622  elmptrab  20828  isfildlem  20858  vtocl2d  28094  ifeqeqx  28147  bnj919  29573  bnj976  29584  bnj1468  29652  bnj110  29664  bnj150  29682  bnj151  29683  bnj607  29722  bnj873  29730  bnj849  29731  bnj1388  29837  setinds  30418  dfon2lem1  30423  tfisg  30451  frinsg  30477  indexdom  31974  sdclem2  31984  sdclem1  31985  fdc1  31988  riotasv2s  32448  sbccomieg  35554  rexrabdioph  35555  rexfrabdioph  35556  aomclem6  35836  pm13.13a  36615  pm13.13b  36616  pm13.14  36617  tratrb  36754  uzwo4  37253  gropd  38795  grstructd  38796