Theorem sbceq1a 3764

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  [wsb 2097  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sbc 3754

This theorem is referenced by:  sbceq2a  3765  elrabsf  3798  cbvralcsf  3903  reusngf  4642  rexreusng  4647  reuprg0  4670  rmosn  4687  rabsnifsb  4690  euotd  5494  reuop  6291  frpoinsg  6341  elfvmptrab1w  7015  elfvmptrab1  7016  ralrnmpt  7089  riotass2  7395  riotass  7396  oprabv  7468  elovmporab  7654  elovmporab1w  7655  elovmporab1  7656  ovmpt3rabdm  7667  elovmpt3rab1  7668  tfisg  7846  tfindes  7855  sbcopeq1a  8042  sbcoteq1a  8044  mpoxopoveq  8211  findcard2  9145  ac6sfi  9240  indexfi  9313  setinds  9714  frinsg  9719  nn0ind-raph  12692  fzrevral  13636  wrdind  14755  wrd2ind  14756  prmind2  16739  elmptrab  23949  isfildlem  23979  2sqreulem4  27580  gropd  29318  grstructd  29319  rspc2daf  32750  opreu2reuALT  32760  ifeqeqx  32825  wrdt2ind  33210  bnj919  35097  bnj976  35107  bnj1468  35175  bnj110  35187  bnj150  35205  bnj151  35206  bnj607  35245  bnj873  35253  bnj849  35254  bnj1388  35362  dfon2lem1  36168  rdgssun  37907  indexdom  38268  sdclem2  38276  sdclem1  38277  fdc1  38280  riotasv2s  39617  elimhyps  39620  sbccomieg  43405  rexrabdioph  43406  rexfrabdioph  43407  aomclem6  43671  pm13.13a  45002  pm13.13b  45003  pm13.14  45004  tratrb  45130  uzwo4  45658  or2expropbilem2  47652  reuf1odnf  47726  ich2exprop  48102  ichnreuop  48103  ichreuopeq  48104  prproropreud  48140  reupr  48153  reuopreuprim  48157