Metamath Proof Explorer

Theorem csbexg

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

Ref Expression
Assertion csbexg ⊢∀xB∈W→⦋A/x⦌B∈V

Proof

Step Hyp Ref Expression
1 df-csb ⊢⦋A/x⦌B=y|[˙A/x]˙y∈B
2 abid2 ⊢y|y∈B=B
3 elex ⊢B∈W→B∈V
4 2 3 eqeltrid ⊢B∈W→y|y∈B∈V
5 4 alimi ⊢∀xB∈W→∀xy|y∈B∈V
6 spsbc ⊢A∈V→∀xy|y∈B∈V→[˙A/x]˙y|y∈B∈V
7 5 6 syl5 ⊢A∈V→∀xB∈W→[˙A/x]˙y|y∈B∈V
8 nfcv ⊢Ⅎ_xV
9 8 sbcabel ⊢A∈V→[˙A/x]˙y|y∈B∈V↔y|[˙A/x]˙y∈B∈V
10 7 9 sylibd ⊢A∈V→∀xB∈W→y|[˙A/x]˙y∈B∈V
11 10 imp ⊢A∈V∧∀xB∈W→y|[˙A/x]˙y∈B∈V
12 1 11 eqeltrid ⊢A∈V∧∀xB∈W→⦋A/x⦌B∈V
13 csbprc ⊢¬A∈V→⦋A/x⦌B=∅
14 0ex ⊢∅∈V
15 13 14 eqeltrdi ⊢¬A∈V→⦋A/x⦌B∈V
16 15 adantr ⊢¬A∈V∧∀xB∈W→⦋A/x⦌B∈V
17 12 16 pm2.61ian ⊢∀xB∈W→⦋A/x⦌B∈V