Theorem sbceq1a 3012

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373  [wsb 1786  [wsbc 3002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-sbc 3003

This theorem is referenced by:  sbceq2a  3013  elrabsf  3041  cbvralcsf  3160  cbvrexcsf  3161  euotd  4307  omsinds  4678  elfvmptrab1  5687  ralrnmpt  5735  rexrnmpt  5736  riotass2  5939  riotass  5940  elovmporab  6159  elovmporab1w  6160  uchoice  6236  sbcopeq1a  6286  mpoxopoveq  6339  findcard2  7001  findcard2s  7002  ac6sfi  7010  opabfi  7050  dcfi  7098  indpi  7475  nn0ind-raph  9510  indstr  9734  fzrevral  10247  exfzdc  10391  zsupcllemstep  10394  infssuzex  10398  uzsinds  10611  wrdind  11198  wrd2ind  11199  prmind2  12517  gropd  15721  grstructd2dom  15722  bj-intabssel  15864  bj-bdfindes  16023  bj-findes  16055