Theorem csbexga 4176

Description: The existence of proper substitution into a class. (Contributed by NM, 10-Nov-2005.)

Assertion

Ref	Expression
csbexga	⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)

Proof of Theorem csbexga

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-csb 3095	. 2 ⊢ ⦋𝐴 / 𝑥⦌𝐵 = {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵}
2		abid2 2327	. . . . . . 7 ⊢ {𝑦 ∣ 𝑦 ∈ 𝐵} = 𝐵
3		elex 2784	. . . . . . 7 ⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V)
4	2, 3	eqeltrid 2293	. . . . . 6 ⊢ (𝐵 ∈ 𝑊 → {𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V)
5	4	alimi 1479	. . . . 5 ⊢ (∀𝑥 𝐵 ∈ 𝑊 → ∀𝑥{𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V)
6		spsbc 3011	. . . . 5 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥{𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V → [𝐴 / 𝑥]{𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V))
7	5, 6	syl5 32	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥 𝐵 ∈ 𝑊 → [𝐴 / 𝑥]{𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V))
8	7	imp 124	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → [𝐴 / 𝑥]{𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V)
9		nfcv 2349	. . . . 5 ⊢ Ⅎ𝑥V
10	9	sbcabel 3081	. . . 4 ⊢ (𝐴 ∈ 𝑉 → ([𝐴 / 𝑥]{𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ∈ V))
11	10	adantr 276	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ([𝐴 / 𝑥]{𝑦 ∣ 𝑦 ∈ 𝐵} ∈ V ↔ {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ∈ V))
12	8, 11	mpbid 147	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → {𝑦 ∣ [𝐴 / 𝑥]𝑦 ∈ 𝐵} ∈ V)
13	1, 12	eqeltrid 2293	1 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 𝐵 ∈ 𝑊) → ⦋𝐴 / 𝑥⦌𝐵 ∈ V)

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105  ∀wal 1371   ∈ wcel 2177  {cab 2192  Vcvv 2773  [wsbc 2999  ⦋csb 3094

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-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-sbc 3000  df-csb 3095

This theorem is referenced by:  csbexa  4177  prdsex  13145  imasex  13181