Theorem sbcied2 3786

Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.)

Hypotheses

Ref	Expression
sbcied2.1	⊢ (𝜑 → 𝐴 ∈ 𝑉)
sbcied2.2	⊢ (𝜑 → 𝐴 = 𝐵)
sbcied2.3	⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))

Assertion

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

Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐵(𝑥)   𝑉(𝑥)

Proof of Theorem sbcied2

Step	Hyp	Ref	Expression
1		sbcied2.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		id 23	. . . 4 ⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴)
3		sbcied2.2	. . . 4 ⊢ (𝜑 → 𝐴 = 𝐵)
4	2, 3	sylan9eqr 2819	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → 𝑥 = 𝐵)
5		sbcied2.3	. . 3 ⊢ ((𝜑 ∧ 𝑥 = 𝐵) → (𝜓 ↔ 𝜒))
6	4, 5	syldan 603	. 2 ⊢ ((𝜑 ∧ 𝑥 = 𝐴) → (𝜓 ↔ 𝜒))
7	1, 6	sbcied 3785	1 ⊢ (𝜑 → ([𝐴 / 𝑥]𝜓 ↔ 𝜒))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  [wsbc 3742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sbc 3743

This theorem is used by:  iscat  17766  sectffval  17845  issubc  17930  isfunc  17959  cat1  18192  ismgm  18737  issgrp  18828  isnsg  19284  isrng  20295  isring  20382  isdomn  20873  islbs  21266  isassa  22077  opsrval  22268  cgrabasimass  29265  isuhgr  29525  isushgr  29526  isupgr  29549  isumgr  29560  isuspgr  29620  isusgr  29621  isgrim  48806  isthinc  50353