Theorem sbceq1a 3815

Description: Equality theorem for class substitution. Class version of sbequ12 2252. (Contributed by NM, 26-Sep-2003.)

Assertion

Ref	Expression
sbceq1a	⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 2256	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
2		dfsbcq2 3807	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	bitr3id 285	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  [wsb 2064  [wsbc 3804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sbc 3805

This theorem is referenced by:  sbceq2a  3816  elrabsf  3853  cbvralcsf  3966  reusngf  4696  rexreusng  4703  reuprg0  4727  rmosn  4744  rabsnifsb  4747  euotd  5532  reuop  6324  frpoinsg  6375  wfisgOLD  6386  elfvmptrab1w  7056  elfvmptrab1  7057  ralrnmpt  7130  riotass2  7435  riotass  7436  oprabv  7510  elovmporab  7696  elovmporab1w  7697  elovmporab1  7698  ovmpt3rabdm  7709  elovmpt3rab1  7710  tfisg  7891  tfindes  7900  sbcopeq1a  8090  sbcoteq1a  8092  mpoxopoveq  8260  findcard2  9230  ac6sfi  9348  indexfi  9430  frinsg  9820  nn0ind-raph  12743  fzrevral  13669  wrdind  14770  wrd2ind  14771  prmind2  16732  elmptrab  23856  isfildlem  23886  2sqreulem4  27516  gropd  29066  grstructd  29067  rspc2daf  32495  opreu2reuALT  32505  ifeqeqx  32565  wrdt2ind  32920  bnj919  34743  bnj976  34753  bnj1468  34822  bnj110  34834  bnj150  34852  bnj151  34853  bnj607  34892  bnj873  34900  bnj849  34901  bnj1388  35009  setinds  35742  dfon2lem1  35747  rdgssun  37344  indexdom  37694  sdclem2  37702  sdclem1  37703  fdc1  37706  riotasv2s  38914  elimhyps  38917  sbccomieg  42749  rexrabdioph  42750  rexfrabdioph  42751  aomclem6  43016  pm13.13a  44376  pm13.13b  44377  pm13.14  44378  tratrb  44507  uzwo4  44955  or2expropbilem2  46948  reuf1odnf  47022  ich2exprop  47345  ichnreuop  47346  ichreuopeq  47347  prproropreud  47383  reupr  47396  reuopreuprim  47400