Theorem sbceq1a 2773

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

Assertion

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

Proof of Theorem sbceq1a

Step	Hyp	Ref	Expression
1		sbid 1657	. 2 ⊢ ([𝑥 / 𝑥]𝜑 ↔ 𝜑)
2		dfsbcq2 2767	. 2 ⊢ (𝑥 = 𝐴 → ([𝑥 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑))
3	1, 2	syl5bbr 183	1 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ [𝐴 / 𝑥]𝜑))

Syntax hints:   → wi 4   ↔ wb 98   = wceq 1243  [wsb 1645  [wsbc 2764

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-sbc 2765

This theorem is referenced by:  sbceq2a  2774  elrabsf  2801  cbvralcsf  2908  cbvrexcsf  2909  euotd  3991  ralrnmpt  5309  rexrnmpt  5310  riotass2  5494  riotass  5495  sbcopeq1a  5813  mpt2xopoveq  5855  findcard2  6346  findcard2s  6347  ac6sfi  6352  indpi  6440  nn0ind-raph  8355  indstr  8536  fzrevral  8967  bj-intabssel  9928  bj-bdfindes  10074  bj-findes  10106