Theorem sbceq1a 3708

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 3700	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	bitr3id 288	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1539  [wsb 2070  [wsbc 3697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-sbc 3698

This theorem is referenced by:  sbceq2a  3709  elrabsf  3742  cbvralcsf  3848  vtocl2dOLD  3854  reusngf  4570  rexreusng  4575  reuprg0  4596  rmosn  4613  rabsnifsb  4616  euotd  5373  reuop  6123  wfisg  6162  elfvmptrab1w  6786  elfvmptrab1  6787  ralrnmpt  6854  riotass2  7139  riotass  7140  oprabv  7209  elovmporab  7388  elovmporab1w  7389  elovmporab1  7390  ovmpt3rabdm  7401  elovmpt3rab1  7402  tfindes  7577  sbcopeq1a  7753  mpoxopoveq  7896  findcard2  8736  findcard2OLD  8794  ac6sfi  8796  indexfi  8866  nn0ind-raph  12122  fzrevral  13042  wrdind  14132  wrd2ind  14133  prmind2  16082  elmptrab  22528  isfildlem  22558  2sqreulem4  26138  gropd  26924  grstructd  26925  rspc2daf  30338  opreu2reuALT  30347  ifeqeqx  30408  wrdt2ind  30750  bnj919  32267  bnj976  32278  bnj1468  32347  bnj110  32359  bnj150  32377  bnj151  32378  bnj607  32417  bnj873  32425  bnj849  32426  bnj1388  32534  sbcoteq1a  33207  setinds  33271  dfon2lem1  33276  tfisg  33303  frpoinsg  33329  frinsg  33338  rdgssun  35076  indexdom  35453  sdclem2  35461  sdclem1  35462  fdc1  35465  riotasv2s  36535  elimhyps  36538  sbccomieg  40108  rexrabdioph  40109  rexfrabdioph  40110  aomclem6  40377  pm13.13a  41485  pm13.13b  41486  pm13.14  41487  tratrb  41616  uzwo4  42061  or2expropbilem2  43992  reuf1odnf  44032  ich2exprop  44357  ichnreuop  44358  ichreuopeq  44359  prproropreud  44395  reupr  44408  reuopreuprim  44412