Theorem sbceq1a 2849

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

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1289   [wsb 1692   [.wsbc 2840

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-sbc 2841

This theorem is referenced by:  sbceq2a  2850  elrabsf  2877  cbvralcsf  2990  cbvrexcsf  2991  euotd  4081  omsinds  4435  ralrnmpt  5441  rexrnmpt  5442  riotass2  5634  riotass  5635  sbcopeq1a  5957  mpt2xopoveq  6005  findcard2  6603  findcard2s  6604  ac6sfi  6612  indpi  6899  nn0ind-raph  8861  indstr  9079  fzrevral  9515  exfzdc  9647  uzsinds  9844  zsupcllemstep  11215  infssuzex  11219  prmind2  11376  bj-intabssel  11644  bj-bdfindes  11799  bj-findes  11831