Theorem sbceq1a 3776

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2064  [wsbc 3765

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 2007  ax-8 2110  ax-9 2118  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sbc 3766

This theorem is referenced by:  sbceq2a  3777  elrabsf  3811  cbvralcsf  3916  reusngf  4650  rexreusng  4655  reuprg0  4678  rmosn  4695  rabsnifsb  4698  euotd  5488  reuop  6282  frpoinsg  6332  wfisgOLD  6343  elfvmptrab1w  7013  elfvmptrab1  7014  ralrnmpt  7086  riotass2  7392  riotass  7393  oprabv  7467  elovmporab  7653  elovmporab1w  7654  elovmporab1  7655  ovmpt3rabdm  7666  elovmpt3rab1  7667  tfisg  7849  tfindes  7858  sbcopeq1a  8048  sbcoteq1a  8050  mpoxopoveq  8218  findcard2  9178  ac6sfi  9292  indexfi  9372  frinsg  9765  nn0ind-raph  12693  fzrevral  13629  wrdind  14740  wrd2ind  14741  prmind2  16704  elmptrab  23765  isfildlem  23795  2sqreulem4  27417  gropd  29010  grstructd  29011  rspc2daf  32447  opreu2reuALT  32458  ifeqeqx  32523  wrdt2ind  32929  bnj919  34798  bnj976  34808  bnj1468  34877  bnj110  34889  bnj150  34907  bnj151  34908  bnj607  34947  bnj873  34955  bnj849  34956  bnj1388  35064  setinds  35796  dfon2lem1  35801  rdgssun  37396  indexdom  37758  sdclem2  37766  sdclem1  37767  fdc1  37770  riotasv2s  38976  elimhyps  38979  sbccomieg  42816  rexrabdioph  42817  rexfrabdioph  42818  aomclem6  43083  pm13.13a  44431  pm13.13b  44432  pm13.14  44433  tratrb  44561  uzwo4  45077  or2expropbilem2  47062  reuf1odnf  47136  ich2exprop  47485  ichnreuop  47486  ichreuopeq  47487  prproropreud  47523  reupr  47536  reuopreuprim  47540