Theorem sbceq1a 3767

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  [wsb 2065  [wsbc 3756

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 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sbc 3757

This theorem is referenced by:  sbceq2a  3768  elrabsf  3802  cbvralcsf  3907  reusngf  4641  rexreusng  4646  reuprg0  4669  rmosn  4686  rabsnifsb  4689  euotd  5476  reuop  6269  frpoinsg  6319  elfvmptrab1w  6998  elfvmptrab1  6999  ralrnmpt  7071  riotass2  7377  riotass  7378  oprabv  7452  elovmporab  7638  elovmporab1w  7639  elovmporab1  7640  ovmpt3rabdm  7651  elovmpt3rab1  7652  tfisg  7833  tfindes  7842  sbcopeq1a  8031  sbcoteq1a  8033  mpoxopoveq  8201  findcard2  9134  ac6sfi  9238  indexfi  9318  frinsg  9711  nn0ind-raph  12641  fzrevral  13580  wrdind  14694  wrd2ind  14695  prmind2  16662  elmptrab  23721  isfildlem  23751  2sqreulem4  27372  gropd  28965  grstructd  28966  rspc2daf  32402  opreu2reuALT  32413  ifeqeqx  32478  wrdt2ind  32882  bnj919  34764  bnj976  34774  bnj1468  34843  bnj110  34855  bnj150  34873  bnj151  34874  bnj607  34913  bnj873  34921  bnj849  34922  bnj1388  35030  setinds  35773  dfon2lem1  35778  rdgssun  37373  indexdom  37735  sdclem2  37743  sdclem1  37744  fdc1  37747  riotasv2s  38958  elimhyps  38961  sbccomieg  42788  rexrabdioph  42789  rexfrabdioph  42790  aomclem6  43055  pm13.13a  44403  pm13.13b  44404  pm13.14  44405  tratrb  44533  uzwo4  45054  or2expropbilem2  47038  reuf1odnf  47112  ich2exprop  47476  ichnreuop  47477  ichreuopeq  47478  prproropreud  47514  reupr  47527  reuopreuprim  47531