Theorem sbceq1a 3061

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

Assertion

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

Proof of Theorem sbceq1a

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   = wceq 1402  [wsb 1815  [wsbc 3051

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-sbc 3052

This theorem is used by:  sbceq2a  3062  elrabsf  3090  cbvralcsf  3210  cbvrexcsf  3211  ifeqeqxdc  3687  rabsnifsb  3777  euotd  4397  omsinds  4771  elfvmptrab1  5804  ralrnmpt  5853  rexrnmpt  5854  riotass2  6070  riotass  6071  elovmporab  6292  elovmporab1w  6293  uchoice  6375  sbcopeq1a  6425  mpoxopoveq  6516  findcard2  7199  findcard2s  7200  ac6sfi  7208  opabfi  7253  dcfi  7320  indpi  7715  nn0ind-raph  9773  indstr  10008  fzrevral  10528  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  uzsinds  10901  wrdind  11515  wrd2ind  11516  prmind2  12922  gropd  16510  grstructd2dom  16511  bj-intabssel  17039  bj-bdfindes  17197  bj-findes  17229