Theorem sbceq1a 3041

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

Assertion

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

Proof of Theorem sbceq1a

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

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1397  [wsb 1810  [wsbc 3031

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-sbc 3032

This theorem is referenced by:  sbceq2a  3042  elrabsf  3070  cbvralcsf  3190  cbvrexcsf  3191  rabsnifsb  3737  euotd  4347  omsinds  4720  elfvmptrab1  5741  ralrnmpt  5789  rexrnmpt  5790  riotass2  6000  riotass  6001  elovmporab  6222  elovmporab1w  6223  uchoice  6300  sbcopeq1a  6350  mpoxopoveq  6406  findcard2  7078  findcard2s  7079  ac6sfi  7087  opabfi  7132  dcfi  7180  indpi  7562  nn0ind-raph  9597  indstr  9827  fzrevral  10340  exfzdc  10487  zsupcllemstep  10490  infssuzex  10494  uzsinds  10707  wrdind  11307  wrd2ind  11308  prmind2  12697  gropd  15904  grstructd2dom  15905  bj-intabssel  16411  bj-bdfindes  16570  bj-findes  16602