Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpt2fvex Unicode version

Theorem mpt2fvex 5829
 Description: Sufficient condition for an operation maps-to notation to be set-like. (Contributed by Mario Carneiro, 3-Jul-2019.)
Hypothesis
Ref Expression
fmpt2.1
Assertion
Ref Expression
mpt2fvex
Distinct variable groups:   ,,   ,,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)   (,)   (,)

Proof of Theorem mpt2fvex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-ov 5515 . 2
2 elex 2566 . . . . . . . . 9
32alimi 1344 . . . . . . . 8
4 vex 2560 . . . . . . . . 9
5 2ndexg 5795 . . . . . . . . 9
6 nfcv 2178 . . . . . . . . . 10
7 nfcsb1v 2882 . . . . . . . . . . 11
87nfel1 2188 . . . . . . . . . 10
9 csbeq1a 2860 . . . . . . . . . . 11
109eleq1d 2106 . . . . . . . . . 10
116, 8, 10spcgf 2635 . . . . . . . . 9
124, 5, 11mp2b 8 . . . . . . . 8
133, 12syl 14 . . . . . . 7
1413alimi 1344 . . . . . 6
15 1stexg 5794 . . . . . . 7
16 nfcv 2178 . . . . . . . 8
17 nfcsb1v 2882 . . . . . . . . 9
1817nfel1 2188 . . . . . . . 8
19 csbeq1a 2860 . . . . . . . . 9
2019eleq1d 2106 . . . . . . . 8
2116, 18, 20spcgf 2635 . . . . . . 7
224, 15, 21mp2b 8 . . . . . 6
2314, 22syl 14 . . . . 5
2423alrimiv 1754 . . . 4