Metamath Proof Explorer

Theorem mpstrcl

Description: The elements of a pre-statement are sets. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis mpstssv.p ⊢ P = mPreSt ⁡ T
Assertion mpstrcl ⊢ D H A ∈ P → D ∈ V ∧ H ∈ V ∧ A ∈ V

Proof

Step Hyp Ref Expression
1 mpstssv.p ⊢ P = mPreSt ⁡ T
2 df-ot ⊢ D H A = D H A
3 1 mpstssv ⊢ P ⊆ V × V × V
4 3 sseli ⊢ D H A ∈ P → D H A ∈ V × V × V
5 2 4 eqeltrrid ⊢ D H A ∈ P → D H A ∈ V × V × V
6 opelxp ⊢ D H ∈ V × V ↔ D ∈ V ∧ H ∈ V
7 6 anbi1i ⊢ D H ∈ V × V ∧ A ∈ V ↔ D ∈ V ∧ H ∈ V ∧ A ∈ V
8 opelxp ⊢ D H A ∈ V × V × V ↔ D H ∈ V × V ∧ A ∈ V
9 df-3an ⊢ D ∈ V ∧ H ∈ V ∧ A ∈ V ↔ D ∈ V ∧ H ∈ V ∧ A ∈ V
10 7 8 9 3bitr4i ⊢ D H A ∈ V × V × V ↔ D ∈ V ∧ H ∈ V ∧ A ∈ V
11 5 10 sylib ⊢ D H A ∈ P → D ∈ V ∧ H ∈ V ∧ A ∈ V