Theorem sbciegft 1949

Description: Conversion of implicit substitution to explicit class substitution, using a bound-variable hypothesis instead of distinct variables. (Closed theorem version of sbciegf 1950.)

Assertion

Ref	Expression
sbciegft	⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → ([A / x]φ ↔ ψ))

Distinct variable group:   x,A

Proof of Theorem sbciegft

Step	Hyp	Ref	Expression
1		sbc5g 1944	. . . 4 ⊢ (A ∈ B → ([A / x]φ ↔ ∃x(x = A ⋀ φ)))
2	1	3ad2ant1 798	. . 3 ⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → ([A / x]φ ↔ ∃x(x = A ⋀ φ)))
3		19.23t 1112	. . . . . 6 ⊢ (∀x(ψ → ∀xψ) → (∀x((x = A ⋀ φ) → ψ) ↔ (∃x(x = A ⋀ φ) → ψ)))
4	3	biimpa 416	. . . . 5 ⊢ ((∀x(ψ → ∀xψ) ⋀ ∀x((x = A ⋀ φ) → ψ)) → (∃x(x = A ⋀ φ) → ψ))
5		bi1 148	. . . . . . . 8 ⊢ ((φ ↔ ψ) → (φ → ψ))
6	5	imim2i 17	. . . . . . 7 ⊢ ((x = A → (φ ↔ ψ)) → (x = A → (φ → ψ)))
7	6	imp3a 361	. . . . . 6 ⊢ ((x = A → (φ ↔ ψ)) → ((x = A ⋀ φ) → ψ))
8	7	19.20i 989	. . . . 5 ⊢ (∀x(x = A → (φ ↔ ψ)) → ∀x((x = A ⋀ φ) → ψ))
9	4, 8	sylan2 451	. . . 4 ⊢ ((∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → (∃x(x = A ⋀ φ) → ψ))
10	9	3adant1 795	. . 3 ⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → (∃x(x = A ⋀ φ) → ψ))
11	2, 10	sylbid 203	. 2 ⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → ([A / x]φ → ψ))
12		19.21t 1111	. . . . . 6 ⊢ (∀x(ψ → ∀xψ) → (∀x(ψ → (x = A → φ)) ↔ (ψ → ∀x(x = A → φ))))
13	12	biimpa 416	. . . . 5 ⊢ ((∀x(ψ → ∀xψ) ⋀ ∀x(ψ → (x = A → φ))) → (ψ → ∀x(x = A → φ)))
14		bi2 149	. . . . . . . 8 ⊢ ((φ ↔ ψ) → (ψ → φ))
15	14	imim2i 17	. . . . . . 7 ⊢ ((x = A → (φ ↔ ψ)) → (x = A → (ψ → φ)))
16	15	com23 32	. . . . . 6 ⊢ ((x = A → (φ ↔ ψ)) → (ψ → (x = A → φ)))
17	16	19.20i 989	. . . . 5 ⊢ (∀x(x = A → (φ ↔ ψ)) → ∀x(ψ → (x = A → φ)))
18	13, 17	sylan2 451	. . . 4 ⊢ ((∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → (ψ → ∀x(x = A → φ)))
19	18	3adant1 795	. . 3 ⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → (ψ → ∀x(x = A → φ)))
20		sbc6g 1945	. . . 4 ⊢ (A ∈ B → ([A / x]φ ↔ ∀x(x = A → φ)))
21	20	3ad2ant1 798	. . 3 ⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → ([A / x]φ ↔ ∀x(x = A → φ)))
22	19, 21	sylibrd 204	. 2 ⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → (ψ → [A / x]φ))
23	11, 22	impbid 514	1 ⊢ ((A ∈ B ⋀ ∀x(ψ → ∀xψ) ⋀ ∀x(x = A → (φ ↔ ψ))) → ([A / x]φ ↔ ψ))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 773  ∀wal 951   = wceq 953   ∈ wcel 955  ∃wex 977  [wsbc 1166

This theorem is referenced by:  sbciegf 1950  csbiegft 2019

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 775  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-sbc 1932

Copyright terms: Public domain