Theorem sbceq1a 3739

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  [wsb 2068  [wsbc 3728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sbc 3729

This theorem is referenced by:  sbceq2a  3740  elrabsf  3774  cbvralcsf  3879  reusngf  4618  rexreusng  4623  reuprg0  4646  rmosn  4663  rabsnifsb  4666  euotd  5467  reuop  6257  frpoinsg  6307  elfvmptrab1w  6975  elfvmptrab1  6976  ralrnmpt  7048  riotass2  7354  riotass  7355  oprabv  7427  elovmporab  7613  elovmporab1w  7614  elovmporab1  7615  ovmpt3rabdm  7626  elovmpt3rab1  7627  tfisg  7805  tfindes  7814  sbcopeq1a  8002  sbcoteq1a  8004  mpoxopoveq  8169  findcard2  9099  ac6sfi  9194  indexfi  9270  setinds  9670  frinsg  9675  nn0ind-raph  12629  fzrevral  13566  wrdind  14684  wrd2ind  14685  prmind2  16654  elmptrab  23792  isfildlem  23822  2sqreulem4  27417  gropd  29100  grstructd  29101  rspc2daf  32535  opreu2reuALT  32546  ifeqeqx  32612  wrdt2ind  33013  bnj919  34910  bnj976  34920  bnj1468  34988  bnj110  35000  bnj150  35018  bnj151  35019  bnj607  35058  bnj873  35066  bnj849  35067  bnj1388  35175  dfon2lem1  35963  rdgssun  37694  indexdom  38055  sdclem2  38063  sdclem1  38064  fdc1  38067  riotasv2s  39404  elimhyps  39407  sbccomieg  43221  rexrabdioph  43222  rexfrabdioph  43223  aomclem6  43487  pm13.13a  44834  pm13.13b  44835  pm13.14  44836  tratrb  44963  uzwo4  45484  or2expropbilem2  47481  reuf1odnf  47555  ich2exprop  47931  ichnreuop  47932  ichreuopeq  47933  prproropreud  47969  reupr  47982  reuopreuprim  47986