Theorem sbceq1a 2824

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 103   = wceq 1284  [wsb 1685  [wsbc 2815

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-sbc 2816

This theorem is referenced by:  sbceq2a  2825  elrabsf  2852  cbvralcsf  2964  cbvrexcsf  2965  euotd  4009  ralrnmpt  5330  rexrnmpt  5331  riotass2  5514  riotass  5515  sbcopeq1a  5833  mpt2xopoveq  5878  findcard2  6373  findcard2s  6374  ac6sfi  6379  indpi  6532  nn0ind-raph  8464  indstr  8681  fzrevral  9122  exfzdc  9249  uzsinds  9428  zsupcllemstep  10341  infssuzex  10345  prmind2  10502  bj-intabssel  10599  bj-bdfindes  10744  bj-findes  10776