This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fabexgOLD

Description: Obsolete version of fabexg as of 9-Jun-2025. (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis fabexg.1 
|- F = { x | ( x : A --> B /\ ph ) }
Assertion fabexgOLD 
|- ( ( A e. C /\ B e. D ) -> F e. _V )

Proof

Step Hyp Ref Expression
1 fabexg.1 
 |-  F = { x | ( x : A --> B /\ ph ) }
2 xpexg 
 |-  ( ( A e. C /\ B e. D ) -> ( A X. B ) e. _V )
3 pwexg 
 |-  ( ( A X. B ) e. _V -> ~P ( A X. B ) e. _V )
4 fssxp 
 |-  ( x : A --> B -> x C_ ( A X. B ) )
5 velpw 
 |-  ( x e. ~P ( A X. B ) <-> x C_ ( A X. B ) )
6 4 5 sylibr 
 |-  ( x : A --> B -> x e. ~P ( A X. B ) )
7 6 anim1i 
 |-  ( ( x : A --> B /\ ph ) -> ( x e. ~P ( A X. B ) /\ ph ) )
8 7 ss2abi 
 |-  { x | ( x : A --> B /\ ph ) } C_ { x | ( x e. ~P ( A X. B ) /\ ph ) }
9 1 8 eqsstri 
 |-  F C_ { x | ( x e. ~P ( A X. B ) /\ ph ) }
10 ssab2 
 |-  { x | ( x e. ~P ( A X. B ) /\ ph ) } C_ ~P ( A X. B )
11 9 10 sstri 
 |-  F C_ ~P ( A X. B )
12 ssexg 
 |-  ( ( F C_ ~P ( A X. B ) /\ ~P ( A X. B ) e. _V ) -> F e. _V )
13 11 12 mpan 
 |-  ( ~P ( A X. B ) e. _V -> F e. _V )
14 2 3 13 3syl 
 |-  ( ( A e. C /\ B e. D ) -> F e. _V )