Theorem sbceq1a 3750

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

Assertion

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

Proof of Theorem sbceq1a

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  [wsb 2099  [wsbc 3739

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sbc 3740

This theorem is used by:  sbceq2a  3751  elrabsf  3784  cbvralcsf  3889  reusngf  4635  rexreusng  4640  reuprg0  4663  rmosn  4680  rabsnifsb  4683  euotd  5486  reuop  6295  frpoinsg  6345  elfvmptrab1w  7019  elfvmptrab1  7020  ralrnmpt  7094  riotass2  7405  riotass  7406  oprabv  7478  elovmporab  7665  elovmporab1w  7666  elovmporab1  7667  ovmpt3rabdm  7678  elovmpt3rab1  7679  tfisg  7863  tfindes  7872  sbcopeq1a  8058  sbcoteq1a  8060  mpoxopoveq  8229  findcard2  9173  ac6sfi  9268  indexfi  9342  setinds  9743  frinsg  9748  nn0ind-raph  12792  fzrevral  13739  wrdind  14864  wrd2ind  14865  prmind2  16853  elmptrab  24139  isfildlem  24169  2sqreulem4  27774  gropd  29602  grstructd  29603  rspc2daf  33056  opreu2reuALT  33066  ifeqeqx  33131  wrdt2ind  33509  bnj919  35391  bnj976  35401  bnj1468  35469  bnj110  35481  bnj150  35499  bnj151  35500  bnj607  35539  bnj873  35547  bnj849  35548  bnj1388  35656  dfon2lem1  36525  rdgssun  38281  indexdom  38648  sdclem2  38656  sdclem1  38657  fdc1  38660  riotasv2s  39995  elimhyps  39998  sbccomieg  43779  rexrabdioph  43780  rexfrabdioph  43781  aomclem6  44045  pm13.13a  45376  pm13.13b  45377  pm13.14  45378  tratrb  45504  uzwo4  46039  or2expropbilem2  48072  reuf1odnf  48146  ich2exprop  48522  ichnreuop  48523  ichreuopeq  48524  prproropreud  48560  reupr  48573  reuopreuprim  48577