Metamath Proof Explorer

Theorem sbciegft

Description: Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf .) (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Assertion sbciegft ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ ↔ ψ

Proof

Step Hyp Ref Expression
1 sbc5 ⊢ [˙A / x]˙ φ ↔ ∃ x x = A ∧ φ
2 biimp ⊢ φ ↔ ψ → φ → ψ
3 2 imim2i ⊢ x = A → φ ↔ ψ → x = A → φ → ψ
4 3 impd ⊢ x = A → φ ↔ ψ → x = A ∧ φ → ψ
5 4 alimi ⊢ ∀ x x = A → φ ↔ ψ → ∀ x x = A ∧ φ → ψ
6 19.23t ⊢ Ⅎ x ψ → ∀ x x = A ∧ φ → ψ ↔ ∃ x x = A ∧ φ → ψ
7 6 biimpa ⊢ Ⅎ x ψ ∧ ∀ x x = A ∧ φ → ψ → ∃ x x = A ∧ φ → ψ
8 5 7 sylan2 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ∃ x x = A ∧ φ → ψ
9 8 3adant1 ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ∃ x x = A ∧ φ → ψ
10 1 9 syl5bi ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ → ψ
11 biimpr ⊢ φ ↔ ψ → ψ → φ
12 11 imim2i ⊢ x = A → φ ↔ ψ → x = A → ψ → φ
13 12 com23 ⊢ x = A → φ ↔ ψ → ψ → x = A → φ
14 13 alimi ⊢ ∀ x x = A → φ ↔ ψ → ∀ x ψ → x = A → φ
15 19.21t ⊢ Ⅎ x ψ → ∀ x ψ → x = A → φ ↔ ψ → ∀ x x = A → φ
16 15 biimpa ⊢ Ⅎ x ψ ∧ ∀ x ψ → x = A → φ → ψ → ∀ x x = A → φ
17 14 16 sylan2 ⊢ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ψ → ∀ x x = A → φ
18 17 3adant1 ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ψ → ∀ x x = A → φ
19 sbc6g ⊢ A ∈ V → [˙A / x]˙ φ ↔ ∀ x x = A → φ
20 19 3ad2ant1 ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ ↔ ∀ x x = A → φ
21 18 20 sylibrd ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → ψ → [˙A / x]˙ φ
22 10 21 impbid ⊢ A ∈ V ∧ Ⅎ x ψ ∧ ∀ x x = A → φ ↔ ψ → [˙A / x]˙ φ ↔ ψ