Theorem sbceq1a 3753

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  [wsb 2089  [wsbc 3742

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3743

This theorem is referenced by:  sbceq2a  3754  elrabsf  3787  cbvralcsf  3892  reusngf  4630  rexreusng  4635  reuprg0  4658  rmosn  4675  rabsnifsb  4678  euotd  5479  reuop  6275  frpoinsg  6325  elfvmptrab1w  6998  elfvmptrab1  6999  ralrnmpt  7072  riotass2  7378  riotass  7379  oprabv  7451  elovmporab  7637  elovmporab1w  7638  elovmporab1  7639  ovmpt3rabdm  7650  elovmpt3rab1  7651  tfisg  7829  tfindes  7838  sbcopeq1a  8025  sbcoteq1a  8027  mpoxopoveq  8193  findcard2  9127  ac6sfi  9222  indexfi  9297  setinds  9698  frinsg  9703  nn0ind-raph  12667  fzrevral  13611  wrdind  14729  wrd2ind  14730  prmind2  16710  elmptrab  23875  isfildlem  23905  2sqreulem4  27506  gropd  29189  grstructd  29190  rspc2daf  32624  opreu2reuALT  32635  ifeqeqx  32701  wrdt2ind  33092  bnj919  35024  bnj976  35034  bnj1468  35102  bnj110  35114  bnj150  35132  bnj151  35133  bnj607  35172  bnj873  35180  bnj849  35181  bnj1388  35289  dfon2lem1  36092  rdgssun  37833  indexdom  38194  sdclem2  38202  sdclem1  38203  fdc1  38206  riotasv2s  39543  elimhyps  39546  sbccomieg  43331  rexrabdioph  43332  rexfrabdioph  43333  aomclem6  43597  pm13.13a  44944  pm13.13b  44945  pm13.14  44946  tratrb  45073  uzwo4  45594  or2expropbilem2  47588  reuf1odnf  47662  ich2exprop  48038  ichnreuop  48039  ichreuopeq  48040  prproropreud  48076  reupr  48089  reuopreuprim  48093