Theorem sbceq1a 3764

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 3756	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	bitr3id 285	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065  [wsbc 3753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3754

This theorem is referenced by:  sbceq2a  3765  elrabsf  3799  cbvralcsf  3904  reusngf  4638  rexreusng  4643  reuprg0  4666  rmosn  4683  rabsnifsb  4686  euotd  5473  reuop  6266  frpoinsg  6316  elfvmptrab1w  6995  elfvmptrab1  6996  ralrnmpt  7068  riotass2  7374  riotass  7375  oprabv  7449  elovmporab  7635  elovmporab1w  7636  elovmporab1  7637  ovmpt3rabdm  7648  elovmpt3rab1  7649  tfisg  7830  tfindes  7839  sbcopeq1a  8028  sbcoteq1a  8030  mpoxopoveq  8198  findcard2  9128  ac6sfi  9231  indexfi  9311  frinsg  9704  nn0ind-raph  12634  fzrevral  13573  wrdind  14687  wrd2ind  14688  prmind2  16655  elmptrab  23714  isfildlem  23744  2sqreulem4  27365  gropd  28958  grstructd  28959  rspc2daf  32395  opreu2reuALT  32406  ifeqeqx  32471  wrdt2ind  32875  bnj919  34757  bnj976  34767  bnj1468  34836  bnj110  34848  bnj150  34866  bnj151  34867  bnj607  34906  bnj873  34914  bnj849  34915  bnj1388  35023  setinds  35766  dfon2lem1  35771  rdgssun  37366  indexdom  37728  sdclem2  37736  sdclem1  37737  fdc1  37740  riotasv2s  38951  elimhyps  38954  sbccomieg  42781  rexrabdioph  42782  rexfrabdioph  42783  aomclem6  43048  pm13.13a  44396  pm13.13b  44397  pm13.14  44398  tratrb  44526  uzwo4  45047  or2expropbilem2  47034  reuf1odnf  47108  ich2exprop  47472  ichnreuop  47473  ichreuopeq  47474  prproropreud  47510  reupr  47523  reuopreuprim  47527