Metamath Proof Explorer


Theorem mapexOLD

Description: Obsolete version of mapex as of 17-Jun-2025. (Contributed by Raph Levien, 4-Dec-2003) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion mapexOLD A C B D f | f : A B V

Proof

Step Hyp Ref Expression
1 fssxp f : A B f A × B
2 1 ss2abi f | f : A B f | f A × B
3 df-pw 𝒫 A × B = f | f A × B
4 2 3 sseqtrri f | f : A B 𝒫 A × B
5 xpexg A C B D A × B V
6 5 pwexd A C B D 𝒫 A × B V
7 ssexg f | f : A B 𝒫 A × B 𝒫 A × B V f | f : A B V
8 4 6 7 sylancr A C B D f | f : A B V