Theorem sbceq1a 3303

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   [wsb 1702   [.wsbc 3292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-sbc 3293

This theorem is referenced by:  sbceq2a  3304  elrabsf  3331  cbvralcsf  3426  rabsnifsb  4050  euotd  4699  ralrnmpt  5960  riotass2  6187  riotass  6188  tfindes  6582  sbcopeq1a  6735  mpt2xopoveq  6845  findcard2  7662  ac6sfi  7666  indexfi  7729  uzindOLD  10846  nn0ind-raph  10852  fzrevral  11660  wrdind  12488  wrd2ind  12489  prmind2  13891  elmptrab  19531  isfildlem  19561  ifeqeqx  26053  setinds  27734  dfon2lem1  27739  tfisg  27808  wfisg  27813  frinsg  27849  indexdom  28775  sdclem2  28785  sdclem1  28786  fdc1  28789  sbccomieg  29278  rexrabdioph  29279  rexfrabdioph  29280  aomclem6  29559  pm13.13a  29808  pm13.13b  29809  pm13.14  29810  elfvmptrab1  30301  oprabv  30304  elovmpt2rab  30305  elovmpt2rab1  30306  ovmpt3rabdm  30309  elovmpt3rab1  30310  tratrb  31559  bnj919  32077  bnj976  32088  bnj1468  32156  bnj110  32168  bnj150  32186  bnj151  32187  bnj607  32226  bnj873  32234  bnj849  32235  bnj1388  32341  riotasv2s  32932