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  5999  riotass  6000  elovmporab  6221  elovmporab1w  6222  uchoice  6299  sbcopeq1a  6349  mpoxopoveq  6405  findcard2  7077  findcard2s  7078  ac6sfi  7086  opabfi  7131  dcfi  7179  indpi  7561  nn0ind-raph  9596  indstr  9826  fzrevral  10339  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  uzsinds  10705  wrdind  11302  wrd2ind  11303  prmind2  12691  gropd  15897  grstructd2dom  15898  bj-intabssel  16385  bj-bdfindes  16544  bj-findes  16576