P. 385 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38401-38500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	confun4 38401	An attempt at derivative. Resisted simplest path to a proof. (Contributed by Jarvin Udandy, 6-Sep-2020.)
|- ph   &    |- ( ( ph -> ps ) -> ps )   &    |- ( ps -> ( ph -> ch ) )   &    |- ( ( ch -> th ) -> ( ( ph -> th ) <-> ps ) )   &    |- ( ta <-> ( ch -> th ) )   &    |- ( et <-> -. ( ch -> ( ch /\ -. ch ) ) )   &    |- ps   &    |- ( ch -> th )   =>    |- ( ch -> ( ps -> ta ) )
Theorem	confun5 38402	An attempt at derivative. Resisted simplest path to a proof. Interesting that ch, th, ta, et were all provable. (Contributed by Jarvin Udandy, 7-Sep-2020.)
|- ph   &    |- ( ( ph -> ps ) -> ps )   &    |- ( ps -> ( ph -> ch ) )   &    |- ( ( ch -> th ) -> ( ( ph -> th ) <-> ps ) )   &    |- ( ta <-> ( ch -> th ) )   &    |- ( et <-> -. ( ch -> ( ch /\ -. ch ) ) )   &    |- ps   &    |- ( ch -> th )   =>    |- ( ch -> ( et <-> ta ) )
Theorem	plcofph 38403	Given, a,b and a "definition" for c, c is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
|- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )   &    |- ph   &    |- ps   =>    |- ch
Theorem	pldofph 38404	Given, a,b c, d, "definition" for e, e is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
|- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )   &    |- ph   &    |- ps   &    |- ch   &    |- th   =>    |- ta
Theorem	plvcofph 38405	Given, a,b,d, and "definitions" for c, e, f: f is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
|- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )   &    |- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )   &    |- ( et <-> ( ch /\ ta ) )   &    |- ph   &    |- ps   &    |- th   =>    |- et
Theorem	plvcofphax 38406	Given, a,b,d, and "definitions" for c, e, f, g: g is demonstrated. (Contributed by Jarvin Udandy, 8-Sep-2020.)
|- ( ch <-> ( ( ( ( ph /\ ps ) <-> ph ) -> ( ph /\ -. ( ph /\ -. ph ) ) ) /\ ( ph /\ -. ( ph /\ -. ph ) ) ) )   &    |- ( ta <-> ( ( ch -> th ) /\ ( ph <-> ch ) /\ ( ( ph -> ps ) -> ( ps <-> th ) ) ) )   &    |- ( et <-> ( ch /\ ta ) )   &    |- ph   &    |- ps   &    |- th   &    |- ( ze <-> -. ( ps /\ -. ta ) )   =>    |- ze
Theorem	plvofpos 38407	rh is derivable because ONLY one of ch, th, ta, et is implied by mu. (Contributed by Jarvin Udandy, 11-Sep-2020.)
|- ( ch <-> ( -. ph /\ -. ps ) )   &    |- ( th <-> ( -. ph /\ ps ) )   &    |- ( ta <-> ( ph /\ -. ps ) )   &    |- ( et <-> ( ph /\ ps ) )   &    |- ( ze <-> ( ( ( ( ( -. ( ( mu -> ch ) /\ ( mu -> th ) ) /\ -. ( ( mu -> ch ) /\ ( mu -> ta ) ) ) /\ -. ( ( mu -> ch ) /\ ( ch -> et ) ) ) /\ -. ( ( mu -> th ) /\ ( mu -> ta ) ) ) /\ -. ( ( mu -> th ) /\ ( mu -> et ) ) ) /\ -. ( ( mu -> ta ) /\ ( mu -> et ) ) ) )   &    |- ( si <-> ( ( ( mu -> ch ) \/ ( mu -> th ) ) \/ ( ( mu -> ta ) \/ ( mu -> et ) ) ) )   &    |- ( rh <-> ( ze /\ si ) )   &    |- ze   &    |- si   =>    |- rh
Theorem	mdandyv0 38408	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> F. )   &    |- ( ta <-> F. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ph ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ph ) )
Theorem	mdandyv1 38409	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> F. )   &    |- ( ta <-> F. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ph ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ph ) )
Theorem	mdandyv2 38410	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> T. )   &    |- ( ta <-> F. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ps ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ph ) )
Theorem	mdandyv3 38411	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> T. )   &    |- ( ta <-> F. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ps ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ph ) )
Theorem	mdandyv4 38412	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> F. )   &    |- ( ta <-> T. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ph ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ph ) )
Theorem	mdandyv5 38413	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> F. )   &    |- ( ta <-> T. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ph ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ph ) )
Theorem	mdandyv6 38414	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> T. )   &    |- ( ta <-> T. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ps ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ph ) )
Theorem	mdandyv7 38415	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> T. )   &    |- ( ta <-> T. )   &    |- ( et <-> F. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ps ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ph ) )
Theorem	mdandyv8 38416	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> F. )   &    |- ( ta <-> F. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ph ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ps ) )
Theorem	mdandyv9 38417	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> F. )   &    |- ( ta <-> F. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ph ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ps ) )
Theorem	mdandyv10 38418	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> T. )   &    |- ( ta <-> F. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ps ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ps ) )
Theorem	mdandyv11 38419	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> T. )   &    |- ( ta <-> F. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ps ) ) /\ ( ta <-> ph ) ) /\ ( et <-> ps ) )
Theorem	mdandyv12 38420	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> F. )   &    |- ( ta <-> T. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ph ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ps ) )
Theorem	mdandyv13 38421	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> F. )   &    |- ( ta <-> T. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ph ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ps ) )
Theorem	mdandyv14 38422	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> F. )   &    |- ( th <-> T. )   &    |- ( ta <-> T. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ph ) /\ ( th <-> ps ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ps ) )
Theorem	mdandyv15 38423	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ph, ps accordingly (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> F. )   &    |- ( ps <-> T. )   &    |- ( ch <-> T. )   &    |- ( th <-> T. )   &    |- ( ta <-> T. )   &    |- ( et <-> T. )   =>    |- ( ( ( ( ch <-> ps ) /\ ( th <-> ps ) ) /\ ( ta <-> ps ) ) /\ ( et <-> ps ) )
Theorem	mdandyvr0 38424	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> ze ) ) /\ ( ta <-> ze ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr1 38425	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> ze ) ) /\ ( ta <-> ze ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr2 38426	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> si ) ) /\ ( ta <-> ze ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr3 38427	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> si ) ) /\ ( ta <-> ze ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr4 38428	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> ze ) ) /\ ( ta <-> si ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr5 38429	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> ze ) ) /\ ( ta <-> si ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr6 38430	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> si ) ) /\ ( ta <-> si ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr7 38431	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> si ) ) /\ ( ta <-> si ) ) /\ ( et <-> ze ) )
Theorem	mdandyvr8 38432	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> ze ) ) /\ ( ta <-> ze ) ) /\ ( et <-> si ) )
Theorem	mdandyvr9 38433	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> ze ) ) /\ ( ta <-> ze ) ) /\ ( et <-> si ) )
Theorem	mdandyvr10 38434	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> si ) ) /\ ( ta <-> ze ) ) /\ ( et <-> si ) )
Theorem	mdandyvr11 38435	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> si ) ) /\ ( ta <-> ze ) ) /\ ( et <-> si ) )
Theorem	mdandyvr12 38436	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> ze ) ) /\ ( ta <-> si ) ) /\ ( et <-> si ) )
Theorem	mdandyvr13 38437	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> ze ) ) /\ ( ta <-> si ) ) /\ ( et <-> si ) )
Theorem	mdandyvr14 38438	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> ze ) /\ ( th <-> si ) ) /\ ( ta <-> si ) ) /\ ( et <-> si ) )
Theorem	mdandyvr15 38439	Given the equivalences set in the hypotheses, there exist a proof where ch, th, ta, et match ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph <-> ze )   &    |- ( ps <-> si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch <-> si ) /\ ( th <-> si ) ) /\ ( ta <-> si ) ) /\ ( et <-> si ) )
Theorem	mdandyvrx0 38440	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ ze ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx1 38441	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ ze ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx2 38442	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ si ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx3 38443	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ si ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx4 38444	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ ze ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx5 38445	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ ze ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx6 38446	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ si ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx7 38447	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ph )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ si ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ ze ) )
Theorem	mdandyvrx8 38448	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ ze ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ si ) )
Theorem	mdandyvrx9 38449	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ ze ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ si ) )
Theorem	mdandyvrx10 38450	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ si ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ si ) )
Theorem	mdandyvrx11 38451	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ph )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ si ) ) /\ ( ta \/_ ze ) ) /\ ( et \/_ si ) )
Theorem	mdandyvrx12 38452	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ ze ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ si ) )
Theorem	mdandyvrx13 38453	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ph )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ ze ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ si ) )
Theorem	mdandyvrx14 38454	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ph )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ ze ) /\ ( th \/_ si ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ si ) )
Theorem	mdandyvrx15 38455	Given the exclusivities set in the hypotheses, there exist a proof where ch, th, ta, et exclude ze, si accordingly (Contributed by Jarvin Udandy, 7-Sep-2016.)
|- ( ph \/_ ze )   &    |- ( ps \/_ si )   &    |- ( ch <-> ps )   &    |- ( th <-> ps )   &    |- ( ta <-> ps )   &    |- ( et <-> ps )   =>    |- ( ( ( ( ch \/_ si ) /\ ( th \/_ si ) ) /\ ( ta \/_ si ) ) /\ ( et \/_ si ) )
Theorem	H15NH16TH15IH16 38456	Given 15 hypotheses and a 16th hypothesis, there exists a proof the 15 imply the 16th. (Contributed by Jarvin Udandy, 8-Sep-2016.)
|- ph   &    |- ps   &    |- ch   &    |- th   &    |- ta   &    |- et   &    |- ze   &    |- si   &    |- rh   &    |- mu   &    |- la   &    |- ka   &    |- jph   &    |- jps   &    |- jch   &    |- jth   =>    |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph /\ ps ) /\ ch ) /\ th ) /\ ta ) /\ et ) /\ ze ) /\ si ) /\ rh ) /\ mu ) /\ la ) /\ ka ) /\ jph ) /\ jps ) /\ jch ) -> jth )
Theorem	dandysum2p2e4 38457	CONTRADICTION PROVED AT 1 + 1 = 2 . Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added which exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). e.g. 1000 would be '1', 0100 would be '2'. 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- ( ph <-> ( th /\ ta ) )   &    |- ( ps <-> ( et /\ ze ) )   &    |- ( ch <-> ( si /\ rh ) )   &    |- ( th <-> F. )   &    |- ( ta <-> F. )   &    |- ( et <-> T. )   &    |- ( ze <-> T. )   &    |- ( si <-> F. )   &    |- ( rh <-> F. )   &    |- ( mu <-> F. )   &    |- ( la <-> F. )   &    |- ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) )   &    |- (jph <-> ( ( et \/_ ze ) \/ ph ) )   &    |- (jps <-> ( ( si \/_ rh ) \/ ps ) )   &    |- (jch <-> ( ( mu \/_ la ) \/ ch ) )   =>    |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph <-> ( th /\ ta ) ) /\ ( ps <-> ( et /\ ze ) ) ) /\ ( ch <-> ( si /\ rh ) ) ) /\ ( th <-> F. ) ) /\ ( ta <-> F. ) ) /\ ( et <-> T. ) ) /\ ( ze <-> T. ) ) /\ ( si <-> F. ) ) /\ ( rh <-> F. ) ) /\ ( mu <-> F. ) ) /\ ( la <-> F. ) ) /\ ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) ) /\ (jph <-> ( ( et \/_ ze ) \/ ph ) ) ) /\ (jps <-> ( ( si \/_ rh ) \/ ps ) ) ) /\ (jch <-> ( ( mu \/_ la ) \/ ch ) ) ) -> ( ( ( ( ka <-> F. ) /\ (jph <-> F. ) ) /\ (jps <-> T. ) ) /\ (jch <-> F. ) ) )
Theorem	mdandysum2p2e4 38458	CONTRADICTION PROVED AT 1 + 1 = 2 . Luckily Mario Carneiro did a successful version of his own. See Mario's Relevant Work: 1.3.14 Half adder and full adder in propositional calculus. Given the right hypotheses we can prove a dandysum of 2+2=4. The qed step is the value '4' in Decimal BEING IMPLIED by the hypotheses. Note: Values that when added which exceed a 4bit value are not supported. Note: Digits begin from left (least) to right (greatest). e.g. 1000 would be '1', 0100 would be '2'. 0010 would be '4'. How to perceive the hypotheses' bits in order: ( th <-> F. ), ( ta <-> F. ) Would be input value X's first bit, and input value Y's first bit. ( et <-> F. ), ( ze <-> F. ) would be input value X's second bit, and input value Y's second bit. In mdandysum2p2e4, one might imagine what jth or jta could be then do the math with their truths. Also limited to the restriction jth, jta are having opposite truths equivalent to the stated truth constants. (Contributed by Jarvin Udandy, 6-Sep-2016.)
|- (jth <-> F. )   &    |- (jta <-> T. )   &    |- ( ph <-> ( th /\ ta ) )   &    |- ( ps <-> ( et /\ ze ) )   &    |- ( ch <-> ( si /\ rh ) )   &    |- ( th <-> jth )   &    |- ( ta <-> jth )   &    |- ( et <-> jta )   &    |- ( ze <-> jta )   &    |- ( si <-> jth )   &    |- ( rh <-> jth )   &    |- ( mu <-> jth )   &    |- ( la <-> jth )   &    |- ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) )   &    |- (jph <-> ( ( et \/_ ze ) \/ ph ) )   &    |- (jps <-> ( ( si \/_ rh ) \/ ps ) )   &    |- (jch <-> ( ( mu \/_ la ) \/ ch ) )   =>    |- ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph <-> ( th /\ ta ) ) /\ ( ps <-> ( et /\ ze ) ) ) /\ ( ch <-> ( si /\ rh ) ) ) /\ ( th <-> F. ) ) /\ ( ta <-> F. ) ) /\ ( et <-> T. ) ) /\ ( ze <-> T. ) ) /\ ( si <-> F. ) ) /\ ( rh <-> F. ) ) /\ ( mu <-> F. ) ) /\ ( la <-> F. ) ) /\ ( ka <-> ( ( th \/_ ta ) \/_ ( th /\ ta ) ) ) ) /\ (jph <-> ( ( et \/_ ze ) \/ ph ) ) ) /\ (jps <-> ( ( si \/_ rh ) \/ ps ) ) ) /\ (jch <-> ( ( mu \/_ la ) \/ ch ) ) ) -> ( ( ( ( ka <-> F. ) /\ (jph <-> F. ) ) /\ (jps <-> T. ) ) /\ (jch <-> F. ) ) )
21.33  Mathbox for Alexander van der Vekens
21.33.1  Double restricted existential uniqueness
21.33.1.1  Restricted quantification (extension)
Theorem	r19.32 38459	Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 2971. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
|- F/ x ph   =>    |- ( A. x e. A ( ph \/ ps ) <-> ( ph \/ A. x e. A ps ) )
Theorem	rexsb 38460*	An equivalent expression for restricted existence, analogous to exsb 2267. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
|- ( E. x e. A ph <-> E. y e. A A. x ( x = y -> ph ) )
Theorem	rexrsb 38461*	An equivalent expression for restricted existence, analogous to exsb 2267. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
|- ( E. x e. A ph <-> E. y e. A A. x e. A ( x = y -> ph ) )
Theorem	2rexsb 38462*	An equivalent expression for double restricted existence, analogous to rexsb 38460. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
|- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B A. x A. y ( ( x = z /\ y = w ) -> ph ) )
Theorem	2rexrsb 38463*	An equivalent expression for double restricted existence, analogous to 2exsb 2268. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
|- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B A. x e. A A. y e. B ( ( x = z /\ y = w ) -> ph ) )
Theorem	cbvral2 38464*	Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 3062. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
|- F/ z ph   &    |- F/ x ch   &    |- F/ w ch   &    |- F/ y ps   &    |- ( x = z -> ( ph <-> ch ) )   &    |- ( y = w -> ( ch <-> ps ) )   =>    |- ( A. x e. A A. y e. B ph <-> A. z e. A A. w e. B ps )
Theorem	cbvrex2 38465*	Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 3063. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
|- F/ z ph   &    |- F/ x ch   &    |- F/ w ch   &    |- F/ y ps   &    |- ( x = z -> ( ph <-> ch ) )   &    |- ( y = w -> ( ch <-> ps ) )   =>    |- ( E. x e. A E. y e. B ph <-> E. z e. A E. w e. B ps )
Theorem	2ralbiim 38466	Split a biconditional and distribute 2 quantifiers, analogous to 2albiim 1747 and ralbiim 2957. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
|- ( A. x e. A A. y e. B ( ph <-> ps ) <-> ( A. x e. A A. y e. B ( ph -> ps ) /\ A. x e. A A. y e. B ( ps -> ph ) ) )
21.33.1.2  The empty set (extension)
Theorem	raaan2 38467*	Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 3907. It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
|- F/ y ph   &    |- F/ x ps   =>    |- ( ( A = (/) <-> B = (/) ) -> ( A. x e. A A. y e. B ( ph /\ ps ) <-> ( A. x e. A ph /\ A. y e. B ps ) ) )
21.33.1.3  Restricted uniqueness and "at most one" quantification
Theorem	rmoimi 38468	Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- ( ph -> ps )   =>    |- ( E* x e. A ps -> E* x e. A ph )
Theorem	2reu5a 38469	Double restricted existential uniqueness in terms of restricted existence and restricted "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.)
|- ( E! x e. A E! y e. B ph <-> ( E. x e. A ( E. y e. B ph /\ E* y e. B ph ) /\ E* x e. A ( E. y e. B ph /\ E* y e. B ph ) ) )
Theorem	reuimrmo 38470	Restricted uniqueness implies restricted "at most one" through implication, analogous to euimmo 2321. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
|- ( A. x e. A ( ph -> ps ) -> ( E! x e. A ps -> E* x e. A ph ) )
Theorem	rmoanim 38471*	Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2328. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
|- F/ x ph   =>    |- ( E* x e. A ( ph /\ ps ) <-> ( ph -> E* x e. A ps ) )
Theorem	reuan 38472*	Introduction of a conjunct into restricted uniqueness quantifier, analogous to euan 2329. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
|- F/ x ph   =>    |- ( E! x e. A ( ph /\ ps ) <-> ( ph /\ E! x e. A ps ) )
21.33.1.4  Analogs to Existential uniqueness (double quantification)
Theorem	2reurex 38473*	Double restricted quantification with existential uniqueness, analogous to 2euex 2343. (Contributed by Alexander van der Vekens, 24-Jun-2017.)
|- ( E! x e. A E. y e. B ph -> E. y e. B E! x e. A ph )
Theorem	2reurmo 38474*	Double restricted quantification with restricted existential uniqueness and restricted "at most one.", analogous to 2eumo 2344. (Contributed by Alexander van der Vekens, 24-Jun-2017.)
|- ( E! x e. A E* y e. B ph -> E* x e. A E! y e. B ph )
Theorem	2reu2rex 38475*	Double restricted existential uniqueness, analogous to 2eu2ex 2345. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
|- ( E! x e. A E! y e. B ph -> E. x e. A E. y e. B ph )
Theorem	2rmoswap 38476*	A condition allowing swap of restricted "at most one" and restricted existential quantifiers, analogous to 2moswap 2346. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
|- ( A. x e. A E* y e. B ph -> ( E* x e. A E. y e. B ph -> E* y e. B E. x e. A ph ) )
Theorem	2rexreu 38477*	Double restricted existential uniqueness implies double restricted uniqueness quantification, analogous to 2exeu 2348. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) -> E! x e. A E! y e. B ph )
Theorem	2reu1 38478*	Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2352. (Contributed by Alexander van der Vekens, 25-Jun-2017.)
|- ( A. x e. A E* y e. B ph -> ( E! x e. A E! y e. B ph <-> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) ) )
Theorem	2reu2 38479*	Double restricted existential uniqueness, analogous to 2eu2 2353. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
|- ( E! y e. B E. x e. A ph -> ( E! x e. A E! y e. B ph <-> E! x e. A E. y e. B ph ) )
Theorem	2reu3 38480*	Double restricted existential uniqueness, analogous to 2eu3 2354. (Contributed by Alexander van der Vekens, 29-Jun-2017.)
|- ( A. x e. A A. y e. B ( E* x e. A ph \/ E* y e. B ph ) -> ( ( E! x e. A E! y e. B ph /\ E! y e. B E! x e. A ph ) <-> ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) ) )
Theorem	2reu4a 38481*	Definition of double restricted existential uniqueness ("exactly one x and exactly one y"), analogous to 2eu4 2355 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 38482). (Contributed by Alexander van der Vekens, 1-Jul-2017.)
|- ( ( A =/= (/) /\ B =/= (/) ) -> ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) ) )
Theorem	2reu4 38482*	Definition of double restricted existential uniqueness ("exactly one x and exactly one y"), analogous to 2eu4 2355. (Contributed by Alexander van der Vekens, 1-Jul-2017.)
|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> ( E. x e. A E. y e. B ph /\ E. z e. A E. w e. B A. x e. A A. y e. B ( ph -> ( x = z /\ y = w ) ) ) )
Theorem	2reu7 38483*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2358. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
|- ( ( E! x e. A E. y e. B ph /\ E! y e. B E. x e. A ph ) <-> E! x e. A E! y e. B ( E. x e. A ph /\ E. y e. B ph ) )
Theorem	2reu8 38484*	Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2359. Curiously, we can put E! on either of the internal conjuncts but not both. We can also commute E! x e. A E! y e. B using 2reu7 38483. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
|- ( E! x e. A E! y e. B ( E. x e. A ph /\ E. y e. B ph ) <-> E! x e. A E! y e. B ( E! x e. A ph /\ E. y e. B ph ) )
21.33.2  Alternative definitions of function's and operation's values The current definition of the value ( F ` A ) of a function F for an argument A (see df-fv 5609) assures that this value is always a set, see fex 6153. This is because this definition can be applied to any classes F and A, and evaluates to the empty set when it is not meaningful (as shown by ndmfv 5905 and fvprc 5875). Although it is very convenient for many theorems on functions and their proofs, there are some cases in which from ( F ` A ) = (/) alone it cannot be decided/derived if ( F ` A ) is meaningful ( F is actually a function which is defined for A and really has the function value (/)) or not. Therefore, additional assumptions are required, such as (/) e/ ran F, (/) e. ran F or Fun F /\ A e. dom F (see, for example, ndmfvrcl 5906). To avoid such an ambiguity, an alternative definition ( F''' A ) (see df-afv 38489) would be possible which evaluates to the universal class ( ( F''' A ) = _V) if it is not meaningful (see afvnfundmuv 38511, ndmafv 38512, afvprc 38516 and nfunsnafv 38514), and which corresponds to the current definition ( ( F ` A ) = ( F''' A )) if it is (see afvfundmfveq 38510). That means ( F''' A ) = _V -> ( F ` A ) = (/) (see afvpcfv0 38518), but ( F ` A ) = (/) -> ( F''' A ) = _V is not generally valid. In the theory of partial functions, it is a common case that F is not defined at A, which also would result in ( F''' A ) = _V. In this context we say ( F''' A ) "is not defined" instead of "is not meaningful". With this definition the following intuitive equivalence holds: ( F''' A ) e. _V <-> " ( F''' A ) is meaningful/defined". An interesting question would be if ( F ` A ) could be replaced by ( F''' A ) in most of the theorems based on function's values. If we look at the (currently 19) proofs using the definition df-fv 5609 of ( F ` A ), we see that analogons for the following 8 theorems can be proven using the alternative definition: fveq1 5880-> afveq1 38506, fveq2 5881-> afveq2 38507, nffv 5888-> nfafv 38508, csbfv12 5916-> csbafv12g , fvres 5895-> afvres 38544, rlimdm 13614-> rlimdmafv 38549, tz6.12-1 5897-> tz6.12-1-afv 38546, fveu 5873-> afveu 38525. 3 theorems proved by directly using df-fv 5609 are within a mathbox (fvsb 36775) or not used (isumclim3 13819, avril1 25898). However, the remaining 8 theorems proved by directly using df-fv 5609 are used more or less often: * fvex 5891: used in about 1750 proofs. * tz6.12-1 5897: root theorem of many theorems which have not a strict analogon, and which are used many times: fvprc 5875 (used in about 127 proofs), tz6.12i 5901 (used - indirectly via fvbr0 5902 and fvrn0 5903- in 18 proofs, and in fvclss 6162 used in fvclex 6779 used in fvresex 6780, which is not used!), dcomex 8884 (used in 4 proofs), ndmfv 5905 (used in 86 proofs) and nfunsn 5912 (used by dffv2 5954 which is not used). * fv2 5876: only used by elfv 5879, which is only used by fv3 5894, which is not used. * dffv3 5877: used by dffv4 5878 (the previous "df-fv"), which now is only used in deprecated (usage discouraged) theorems or within mathboxes (csbfv12gALTOLD 37186, csbfv12gALTVD 37269), by shftval 13137 (itself used in 9 proofs), by dffv5 30696 (mathbox) and by fvco2 5956, which has the analogon afvco2 38548. * fvopab5 5989: used only by ajval 26501 (not used) and by adjval 27541 ( used - indirectly - in 9 proofs). * zsum 13783: used (via isum 13784, sum0 13786 and fsumsers 13793) in more than 90 proofs. * isumshft 13896: used in pserdv2 23383 and (via logtayl 23603) 4 other proofs. * ovtpos 6999: used in 14 proofs. As a result of this analysis we can say that the current definition of a function's value is crucial for Metamath and cannot be exchanged easily with an alternative definition. While fv2 5876, dffv3 5877, fvopab5 5989, zsum 13783, isumshft 13896 and ovtpos 6999 are not critical or are, hopefully, also valid for the alternative definition, fvex 5891 and tz6.12-1 5897 (and the theorems based on them) are essential for the current definition of function values. With the same arguments, an alternatvie definition of operation's values (( A O B)) could be meaningful to avoid ambiguities, see df-aov 38490. For additional discussions/material see https://groups.google.com/forum/#!topic/metamath/cteNUppB6A4.
Syntax	wdfat 38485	Extend the definition of a wff to include the "defined at" predicate. (Read: (The Function) F is defined at (the argument) A). In a previous version, the token "def@" was used. However, since the @ is used (informally) as a replacement for $ in commented out sections that may be deleted some day. While there is no violation of any standard to use the @ in a token, it could make the search for such commented-out sections slightly more difficult. (See remark of Norman Megill at https://groups.google.com/forum/#!topic/metamath/cteNUppB6A4).
wff F defAt A
Syntax	cafv 38486	Extend the definition of a class to include the value of a function. (Read: The value of F at A, or " F of A."). In a previous version, the symbol " ' " was used. However, since the similarity with the symbol ` used for the current definition of a function's value (see df-fv 5609), which, by the way, was intended to visualize that in many cases ` and " ' " are exchangeable, makes reading the theorems, especially those which uses both definitions as dfafv2 38504, very difficult, 3 apostrophes ''' are used now so that it's easier to distinguish from df-fv 5609 and df-ima 4866. And not three backticks ( three times ` ) since that would be annoying to escape in a comment. (See remark of Norman Megill and Gerard Lang at https://groups.google.com/forum/#!topic/metamath/cteNUppB6A4).
class ( F''' A )
Syntax	caov 38487	Extend class notation to include the value of an operation F (such as +) for two arguments A and B. Note that the syntax is simply three class symbols in a row surrounded by a pair of parentheses in contrast to the current definition, see df-ov 6308.
class (( A F B))
Definition	df-dfat 38488	Definition of the predicate that determines if some class F is defined as function for an argument A or, in other words, if the function value for some class F for an argument A is defined. We say that F is defined at A if a F is a function restricted to the member A of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( F defAt A <-> ( A e. dom F /\ Fun ( F |` { A } ) ) )
Definition	df-afv 38489*	Alternative definition of the value of a function, ( F''' A ), also known as function application. In contrast to ( F ` A ) = (/) (see df-fv 5609 and ndmfv 5905), ( F''' A ) = _V if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.)
|- ( F''' A ) = if ( F defAt A , ( iota x A F x ) , _V )
Definition	df-aov 38490	Define the value of an operation. In contrast to df-ov 6308, the alternative definition for a function value (see df-afv 38489) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation F and its arguments A and B- will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- (( A F B)) = ( F''' <. A , B >. )
21.33.2.1  Restricted quantification (extension)
Theorem	ralbinrald 38491*	Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.)
|- ( ph -> X e. A )   &    |- ( x e. A -> x = X )   &    |- ( x = X -> ( ps <-> th ) )   =>    |- ( ph -> ( A. x e. A ps <-> th ) )
21.33.2.2  The universal class (extension)
Theorem	nvelim 38492	If a class is the universal class it doesn't belong to any class, generalisation of nvel 4563. (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( A = _V -> -. A e. B )
21.33.2.3  Introduce the Axiom of Power Sets (extension)
Theorem	alneu 38493	If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017.)
|- ( A. x ph -> -. E! x ph )
Theorem	eu2ndop1stv 38494*	If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
|- ( E! y <. A , y >. e. V -> A e. _V )
21.33.2.4  Relations (extension)
Theorem	eldmressn 38495	Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.)
|- ( B e. dom ( F |` { A } ) -> B = A )
21.33.2.5  Functions (extension)
Theorem	fveqvfvv 38496	If a function's value at an argument is the universal class (which can never be the case because of fvex 5891), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything (see pm2.21i 134). (Contributed by Alexander van der Vekens, 26-May-2017.)
|- ( ( F ` A ) = _V -> ( F ` A ) = B )
Theorem	funresfunco 38497	Composition of two functions, generalization of funco 5639. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
|- ( ( Fun ( F |` ran G ) /\ Fun G ) -> Fun ( F o. G ) )
Theorem	fnresfnco 38498	Composition of two functions, similar to fnco 5702. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
|- ( ( ( F |` ran G ) Fn ran G /\ G Fn B ) -> ( F o. G ) Fn B )
Theorem	funcoressn 38499	A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
|- ( ( ( ( G ` X ) e. dom F /\ Fun ( F |` { ( G ` X ) } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( ( F o. G ) |` { X } ) )
Theorem	funressnfv 38500	A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.)
|- ( ( ( X e. dom ( F o. G ) /\ Fun ( ( F o. G ) |` { X } ) ) /\ ( G Fn A /\ X e. A ) ) -> Fun ( F |` { ( G ` X ) } ) )