Theorem sbceqbid 3798

Description: Equality theorem for class substitution. (Contributed by Thierry Arnoux, 4-Sep-2018.)

Hypotheses

Ref	Expression
sbceqbid.1	⊢ (𝜑 → 𝐴 = 𝐵)
sbceqbid.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
sbceqbid	⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem sbceqbid

Step	Hyp	Ref	Expression
1		sbceqbid.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		sbceqbid.2	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	abbidv 2806	. . 3 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒})
4	1, 3	eleq12d 2833	. 2 ⊢ (𝜑 → (𝐴 ∈ {𝑥 ∣ 𝜓} ↔ 𝐵 ∈ {𝑥 ∣ 𝜒}))
5		df-sbc 3792	. 2 ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝐴 ∈ {𝑥 ∣ 𝜓})
6		df-sbc 3792	. 2 ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝐵 ∈ {𝑥 ∣ 𝜒})
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ [𝐵 / 𝑥]𝜒))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537   ∈ wcel 2106  {cab 2712  [wsbc 3791

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-sbc 3792

This theorem is referenced by:  sbcbidv  3851  frpoins3xpg  8164  frpoins3xp3g  8165  fpwwe2cbv  10668  fpwwe2lem2  10670  fpwwe2lem3  10671  fi1uzind  14543  isprs  18354  isdrs  18359  istos  18476  isdlat  18580  issrg  20206  islmod  20879  fdc  37732  hdmap1ffval  41778  hdmap1fval  41779  hdmapffval  41809  hdmapfval  41810  hgmapffval  41868  hgmapfval  41869  sbccomieg  42781  rexrabdioph  42782