Theorem sbceq1a 3802

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  [wsb 2062  [wsbc 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792

This theorem is referenced by:  sbceq2a  3803  elrabsf  3840  cbvralcsf  3953  reusngf  4679  rexreusng  4684  reuprg0  4707  rmosn  4724  rabsnifsb  4727  euotd  5523  reuop  6315  frpoinsg  6366  wfisgOLD  6377  elfvmptrab1w  7043  elfvmptrab1  7044  ralrnmpt  7116  riotass2  7418  riotass  7419  oprabv  7493  elovmporab  7679  elovmporab1w  7680  elovmporab1  7681  ovmpt3rabdm  7692  elovmpt3rab1  7693  tfisg  7875  tfindes  7884  sbcopeq1a  8073  sbcoteq1a  8075  mpoxopoveq  8243  findcard2  9203  ac6sfi  9318  indexfi  9398  frinsg  9789  nn0ind-raph  12716  fzrevral  13649  wrdind  14757  wrd2ind  14758  prmind2  16719  elmptrab  23851  isfildlem  23881  2sqreulem4  27513  gropd  29063  grstructd  29064  rspc2daf  32495  opreu2reuALT  32505  ifeqeqx  32563  wrdt2ind  32923  bnj919  34760  bnj976  34770  bnj1468  34839  bnj110  34851  bnj150  34869  bnj151  34870  bnj607  34909  bnj873  34917  bnj849  34918  bnj1388  35026  setinds  35760  dfon2lem1  35765  rdgssun  37361  indexdom  37721  sdclem2  37729  sdclem1  37730  fdc1  37733  riotasv2s  38940  elimhyps  38943  sbccomieg  42781  rexrabdioph  42782  rexfrabdioph  42783  aomclem6  43048  pm13.13a  44403  pm13.13b  44404  pm13.14  44405  tratrb  44534  uzwo4  44993  or2expropbilem2  46983  reuf1odnf  47057  ich2exprop  47396  ichnreuop  47397  ichreuopeq  47398  prproropreud  47434  reupr  47447  reuopreuprim  47451