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

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

Proof of Theorem mpofvex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 df-ov 5784 . 2
2 elex 2700 . . . . . . . . 9
32alimi 1432 . . . . . . . 8
4 vex 2692 . . . . . . . . 9
5 2ndexg 6073 . . . . . . . . 9
6 nfcv 2282 . . . . . . . . . 10
7 nfcsb1v 3039 . . . . . . . . . . 11
87nfel1 2293 . . . . . . . . . 10
9 csbeq1a 3015 . . . . . . . . . . 11
109eleq1d 2209 . . . . . . . . . 10
116, 8, 10spcgf 2771 . . . . . . . . 9
124, 5, 11mp2b 8 . . . . . . . 8
133, 12syl 14 . . . . . . 7
1413alimi 1432 . . . . . 6
15 1stexg 6072 . . . . . . 7
16 nfcv 2282 . . . . . . . 8
17 nfcsb1v 3039 . . . . . . . . 9
1817nfel1 2293 . . . . . . . 8
19 csbeq1a 3015 . . . . . . . . 9
2019eleq1d 2209 . . . . . . . 8
2116, 18, 20spcgf 2771 . . . . . . 7
224, 15, 21mp2b 8 . . . . . 6
2314, 22syl 14 . . . . 5
2423alrimiv 1847 . . . 4