Theorem sbceq1a 3039

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1395  [wsb 1808  [wsbc 3029

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-sbc 3030

This theorem is referenced by:  sbceq2a  3040  elrabsf  3068  cbvralcsf  3188  cbvrexcsf  3189  rabsnifsb  3735  euotd  4345  omsinds  4718  elfvmptrab1  5737  ralrnmpt  5785  rexrnmpt  5786  riotass2  5995  riotass  5996  elovmporab  6217  elovmporab1w  6218  uchoice  6295  sbcopeq1a  6345  mpoxopoveq  6401  findcard2  7071  findcard2s  7072  ac6sfi  7080  opabfi  7123  dcfi  7171  indpi  7552  nn0ind-raph  9587  indstr  9817  fzrevral  10330  exfzdc  10476  zsupcllemstep  10479  infssuzex  10483  uzsinds  10696  wrdind  11293  wrd2ind  11294  prmind2  12682  gropd  15888  grstructd2dom  15889  bj-intabssel  16321  bj-bdfindes  16480  bj-findes  16512