Metamath Proof Explorer

Theorem xp0OLD

Description: Obsolete version of xp0 as of 1-Feb-2026. (Contributed by NM, 12-Apr-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion xp0OLD 
|- ( A X. (/) ) = (/)

Proof

Step Hyp Ref Expression
1 0xp 
 |-  ( (/) X. A ) = (/)
2 1 cnveqi 
 |-  `' ( (/) X. A ) = `' (/)
3 cnvxp 
 |-  `' ( (/) X. A ) = ( A X. (/) )
4 cnv0 
 |-  `' (/) = (/)
5 2 3 4 3eqtr3i 
 |-  ( A X. (/) ) = (/)