Metamath Proof Explorer

Theorem xp1en

Description: One times a cardinal number. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion xp1en 
|- ( A e. V -> ( A X. 1o ) ~~ A )

Proof

Step Hyp Ref Expression
1 df1o2 
 |-  1o = { (/) }
2 1 xpeq2i 
 |-  ( A X. 1o ) = ( A X. { (/) } )
3 0ex 
 |-  (/) e. _V
4 xpsneng 
 |-  ( ( A e. V /\ (/) e. _V ) -> ( A X. { (/) } ) ~~ A )
5 3 4 mpan2 
 |-  ( A e. V -> ( A X. { (/) } ) ~~ A )
6 2 5 eqbrtrid 
 |-  ( A e. V -> ( A X. 1o ) ~~ A )