Theorem sbceq1a 3755

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sbc 3745

This theorem is referenced by:  sbceq2a  3756  elrabsf  3790  cbvralcsf  3895  reusngf  4628  rexreusng  4633  reuprg0  4656  rmosn  4673  rabsnifsb  4676  euotd  5460  reuop  6245  frpoinsg  6295  elfvmptrab1w  6961  elfvmptrab1  6962  ralrnmpt  7034  riotass2  7340  riotass  7341  oprabv  7413  elovmporab  7599  elovmporab1w  7600  elovmporab1  7601  ovmpt3rabdm  7612  elovmpt3rab1  7613  tfisg  7794  tfindes  7803  sbcopeq1a  7991  sbcoteq1a  7993  mpoxopoveq  8159  findcard2  9088  ac6sfi  9189  indexfi  9269  frinsg  9666  nn0ind-raph  12594  fzrevral  13533  wrdind  14646  wrd2ind  14647  prmind2  16614  elmptrab  23730  isfildlem  23760  2sqreulem4  27381  gropd  28994  grstructd  28995  rspc2daf  32428  opreu2reuALT  32439  ifeqeqx  32504  wrdt2ind  32908  bnj919  34736  bnj976  34746  bnj1468  34815  bnj110  34827  bnj150  34845  bnj151  34846  bnj607  34885  bnj873  34893  bnj849  34894  bnj1388  35002  setinds  35754  dfon2lem1  35759  rdgssun  37354  indexdom  37716  sdclem2  37724  sdclem1  37725  fdc1  37728  riotasv2s  38939  elimhyps  38942  sbccomieg  42769  rexrabdioph  42770  rexfrabdioph  42771  aomclem6  43035  pm13.13a  44383  pm13.13b  44384  pm13.14  44385  tratrb  44513  uzwo4  45034  or2expropbilem2  47021  reuf1odnf  47095  ich2exprop  47459  ichnreuop  47460  ichreuopeq  47461  prproropreud  47497  reupr  47510  reuopreuprim  47514