Theorem sbceq1a 2996

Description: Equality theorem for class substitution. Class version of sbequ12 1782. (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 1785	. 2 |- ( [ x / x ] ph <-> ph )
2		dfsbcq2 2989	. 2 |- ( x = A -> ( [ x / x ] ph <-> [. A / x ]. ph ) )
3	1, 2	bitr3id 194	1 |- ( x = A -> ( ph <-> [. A / x ]. ph ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1364   [wsb 1773   [.wsbc 2986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-sbc 2987

This theorem is referenced by:  sbceq2a  2997  elrabsf  3025  cbvralcsf  3144  cbvrexcsf  3145  euotd  4284  omsinds  4655  elfvmptrab1  5653  ralrnmpt  5701  rexrnmpt  5702  riotass2  5901  riotass  5902  elovmporab  6120  elovmporab1w  6121  uchoice  6192  sbcopeq1a  6242  mpoxopoveq  6295  findcard2  6947  findcard2s  6948  ac6sfi  6956  opabfi  6994  dcfi  7042  indpi  7404  nn0ind-raph  9437  indstr  9661  fzrevral  10174  exfzdc  10310  uzsinds  10518  zsupcllemstep  12085  infssuzex  12089  prmind2  12261  bj-intabssel  15351  bj-bdfindes  15511  bj-findes  15543