Theorem sbceq1a 3787

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1534  [wsb 2060  [wsbc 3776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-sbc 3777

This theorem is referenced by:  sbceq2a  3788  elrabsf  3825  cbvralcsf  3937  reusngf  4677  rexreusng  4684  reuprg0  4707  rmosn  4724  rabsnifsb  4727  euotd  5515  reuop  6297  frpoinsg  6349  wfisgOLD  6360  elfvmptrab1w  7032  elfvmptrab1  7033  ralrnmpt  7106  riotass2  7407  riotass  7408  oprabv  7480  elovmporab  7667  elovmporab1w  7668  elovmporab1  7669  ovmpt3rabdm  7680  elovmpt3rab1  7681  tfisg  7858  tfindes  7867  sbcopeq1a  8053  sbcoteq1a  8055  mpoxopoveq  8225  findcard2  9189  findcard2OLD  9309  ac6sfi  9312  indexfi  9385  frinsg  9775  nn0ind-raph  12693  fzrevral  13619  wrdind  14705  wrd2ind  14706  prmind2  16656  elmptrab  23744  isfildlem  23774  2sqreulem4  27400  gropd  28857  grstructd  28858  rspc2daf  32279  opreu2reuALT  32288  ifeqeqx  32346  wrdt2ind  32687  bnj919  34398  bnj976  34408  bnj1468  34477  bnj110  34489  bnj150  34507  bnj151  34508  bnj607  34547  bnj873  34555  bnj849  34556  bnj1388  34664  setinds  35374  dfon2lem1  35379  rdgssun  36857  indexdom  37207  sdclem2  37215  sdclem1  37216  fdc1  37219  riotasv2s  38430  elimhyps  38433  sbccomieg  42213  rexrabdioph  42214  rexfrabdioph  42215  aomclem6  42483  pm13.13a  43844  pm13.13b  43845  pm13.14  43846  tratrb  43975  uzwo4  44417  or2expropbilem2  46415  reuf1odnf  46487  ich2exprop  46811  ichnreuop  46812  ichreuopeq  46813  prproropreud  46849  reupr  46862  reuopreuprim  46866