Theorem sbceq1a 3185

Description: Equality theorem for class substitution. Class version of sbequ12 1935. (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 1939	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 3178	. 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 1362   [wsb 1699   [.wsbc 3175

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-sbc 3176

This theorem is referenced by:  sbceq2a  3186  elrabsf  3213  cbvralcsf  3307  rabsnifsb  3931  euotd  4580  ralrnmpt  5840  riotass2  6067  riotass  6068  tfindes  6462  sbcopeq1a  6615  mpt2xopoveq  6725  findcard2  7540  ac6sfi  7544  indexfi  7607  uzindOLD  10724  nn0ind-raph  10730  fzrevral  11528  wrdind  12355  wrd2ind  12356  prmind2  13757  elmptrab  19242  isfildlem  19272  ifeqeqx  25726  setinds  27438  dfon2lem1  27443  tfisg  27512  wfisg  27517  frinsg  27553  indexdom  28472  sdclem2  28482  sdclem1  28483  fdc1  28486  sbccomieg  28976  rexrabdioph  28977  rexfrabdioph  28978  aomclem6  29257  pm13.13a  29506  pm13.13b  29507  pm13.14  29508  elfvmptrab1  30000  oprabv  30003  elovmpt2rab  30004  elovmpt2rab1  30005  ovmpt3rabdm  30008  elovmpt3rab1  30009  tratrb  30943  bnj919  31462  bnj976  31473  bnj1468  31541  bnj110  31553  bnj150  31571  bnj151  31572  bnj607  31611  bnj873  31619  bnj849  31620  bnj1388  31726  riotasv2s  32182