Theorem sbceq1a 2825

Description: Equality theorem for class substitution. Class version of sbequ12 1695. (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 1698	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 2819	. 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 1285   [wsb 1686   [.wsbc 2816

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 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064

This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-sbc 2817

This theorem is referenced by:  sbceq2a  2826  elrabsf  2853  cbvralcsf  2965  cbvrexcsf  2966  euotd  4011  ralrnmpt  5335  rexrnmpt  5336  riotass2  5519  riotass  5520  sbcopeq1a  5838  mpt2xopoveq  5883  findcard2  6413  findcard2s  6414  ac6sfi  6421  indpi  6583  nn0ind-raph  8534  indstr  8751  fzrevral  9187  exfzdc  9315  uzsinds  9507  zsupcllemstep  10474  infssuzex  10478  prmind2  10635  bj-intabssel  10735  bj-bdfindes  10887  bj-findes  10919